Nuprl Definition : iff
P ⇐⇒ Q == (P ⇒ Q) ∧ (P ⇐ Q)
Definitions occuring in Statement :
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
implies: P ⇒ Q,
rev_implies: P ⇐ Q
Rules referencing :
sqequalExtensionalEquality,
sqleExtensionalEquality
FDL editor aliases :
iff
Latex:
P \mLeftarrow{}{}\mRightarrow{} Q == (P {}\mRightarrow{} Q) \mwedge{} (P \mLeftarrow{}{} Q)
Date html generated:
2016_05_13-PM-03_04_18
Last ObjectModification:
2015_09_22-PM-05_43_40
Theory : core_1
Home
Index