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

Theorem bi2 128
 Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
bi2 ((𝜑𝜓) → (𝜓𝜑))

Proof of Theorem bi2
StepHypRef Expression
1 df-bi 115 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 109 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
32simprd 112 1 ((𝜑𝜓) → (𝜓𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  bicom1  129  pm5.74  177  bi3ant  222  pm5.32d  438  nbn2  646  pm4.72  770  con4biddc  788  con1biimdc  801  bijadc  810  pclem6  1306  exbir  1366  simplbi2comg  1373  albi  1398  exbi  1536  equsexd  1658  cbv2h  1675  sbiedh  1711  ceqsalt  2626  spcegft  2678  elab3gf  2744  euind  2780  reu6  2782  reuind  2796  sbciegft  2845  iota4  4915  fv3  5229  algcvgblem  10575  bj-notbi  10874  bj-inf2vnlem1  10923
 Copyright terms: Public domain W3C validator