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

Theorem bi2 129
 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 116 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 110 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
32simprd 113 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  ax-ia2 106 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  bicom1  130  pm5.74  178  bi3ant  223  pm5.32d  445  notbi  655  nbn2  686  pm4.72  812  con4biddc  842  con1biimdc  858  bijadc  867  pclem6  1352  exbir  1412  simplbi2comg  1419  albi  1444  exbi  1583  equsexd  1707  cbv2h  1724  sbiedh  1760  ceqsalt  2712  spcegft  2765  elab3gf  2834  euind  2871  reu6  2873  reuind  2889  sbciegft  2939  iota4  5109  fv3  5447  algcvgblem  11753  bj-inf2vnlem1  13312
 Copyright terms: Public domain W3C validator