Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bi1 GIF version

Theorem bi1 117
 Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
bi1 ((𝜑𝜓) → (𝜑𝜓))

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 116 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 110 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
32simpld 111 1 ((𝜑𝜓) → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  biimpi  119  bicom1  130  biimpd  143  ibd  177  pm5.74  178  bi3ant  223  pm5.501  243  pm5.32d  446  notbi  656  pm5.19  696  con4biddc  843  con1biimdc  859  bijadc  868  pclem6  1353  albi  1445  exbi  1584  equsexd  1708  cbv2h  1725  sbiedh  1761  eumo0  2031  ceqsalt  2716  vtoclgft  2740  spcgft  2767  pm13.183  2827  reu6  2878  reu3  2879  sbciegft  2944  ddifstab  3214  exmidsssnc  4135  fv3  5453  prnmaxl  7340  prnminu  7341  elabgft1  13176  elabgf2  13178  bj-axemptylem  13281  bj-inf2vn  13363  bj-inf2vn2  13364  bj-nn0sucALT  13367
 Copyright terms: Public domain W3C validator