Nuprl Rule : andLevelFunctionality

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

  BY andLevelFunctionality #$i v w ()

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

Latex:
H x:(P \mwedge{} Q \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} A \mwedge{} B \mmember{} \mBbbU{}\{lvl\} ext experimental\{andLevelFunctionality\}(Ax) BY andLevelFunctionality \#\$i v w () H v:(P \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} A \mmember{} \mBbbU{}\{lvl\} H v:P, 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