Nuprl Definition : face-term-iff
Gamma ⊢ (phi ⇐⇒ psi) == Gamma ⊢ (phi ⇒ psi) ∧ Gamma ⊢ (psi ⇒ phi)
Definitions occuring in Statement :
face-term-implies: Gamma ⊢ (phi ⇒ psi),
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
face-term-implies: Gamma ⊢ (phi ⇒ psi)
FDL editor aliases :
face-term-iff
Latex:
Gamma \mvdash{} (phi \mLeftarrow{}{}\mRightarrow{} psi) == Gamma \mvdash{} (phi {}\mRightarrow{} psi) \mwedge{} Gamma \mvdash{} (psi {}\mRightarrow{} phi)
Date html generated:
2016_05_19-AM-08_29_15
Last ObjectModification:
2016_03_04-PM-11_40_55
Theory : cubical!type!theory
Home
Index