Nuprl Rule : sqequalElimination

H x:(p ~ q), J ⊢ C ext t

  BY sqequalElimination #$i
  
  H x:(p ~ q), J[Ax/x] ⊢ C[Ax/x] ext t


Definitions occuring in rule :  sqequal: s ~ t,  axiom: Ax
Latex:
H  x:(p  \msim{}  q),  J  \mvdash{}  C  ext  t

    BY  sqequalElimination  \#\$i
   
    H  x:(p  \msim{}  q),  J[Ax/x]  \mvdash{}  C[Ax/x]  ext  t


Date html generated: 2019_06_20-PM-04_12_01
Last ObjectModification: 2015_11_24-PM-01_51_59

Theory : rules


Home Index