Nuprl Rule : impliesLevelFunctionality

H x:(P ⇒ Q ∈ 𝕌{lvl}), J ⊢ A ⇒ B ∈ 𝕌{lvl} ext experimental{impliesLevelFunctionality}(Ax)

  BY impliesLevelFunctionality #$i v w ()

  H v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:A, w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}
  H v:(P ∈ 𝕌{lvl}), w:A @lvl, J ⊢ P

Latex:
H x:(P {}\mRightarrow{} Q \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} A {}\mRightarrow{} B \mmember{} \mBbbU{}\{lvl\} ext experimental\{impliesLevelFunctionality\}(Ax) BY impliesLevelFunctionality \#\$i v w () H v:(P \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} A \mmember{} \mBbbU{}\{lvl\} H v:A, w:(Q \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} B \mmember{} \mBbbU{}\{lvl\} H v:(P \mmember{} \mBbbU{}\{lvl\}), w:A @lvl, J \mvdash{} P Date html generated: 2019_06_20-PM-04_11_53 Last ObjectModification: 2016_01_12-PM-01_16_33 Theory : rules Home Index