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

Theorem bi2 121
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 110 . . 3 (((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
21simpli 104 . 2 ((φψ) → ((φψ) (ψφ)))
32simprd 107 1 ((φψ) → (ψφ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bicom1  122  pm5.74  168  bi3ant  213  pm5.32d  423  nbn2  612  pm4.72  735  con4biddc  753  con1biimdc  766  bijadc  775  pclem6  1264  exbir  1322  simplbi2comg  1329  albi  1354  exbi  1492  equsexd  1614  cbv2h  1631  sbiedh  1667  ceqsalt  2574  spcegft  2626  elab3gf  2686  euind  2722  reu6  2724  reuind  2738  sbciegft  2787  iota4  4828  fv3  5140  bj-notbi  9356  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator