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

Theorem bi1 111
 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 110 . . 3 (((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
21simpli 104 . 2 ((φψ) → ((φψ) (ψφ)))
32simpld 105 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 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  biimpi  113  bicom1  122  biimpd  132  ibd  167  pm5.74  168  bi3ant  213  pm5.501  233  pm5.32d  423  pm5.19  621  con4biddc  753  con1biimdc  766  bijadc  775  pclem6  1264  albi  1354  exbi  1492  equsexd  1614  cbv2h  1631  sbiedh  1667  eumo0  1928  ceqsalt  2574  vtoclgft  2598  spcgft  2624  pm13.183  2675  reu6  2724  reu3  2725  sbciegft  2787  fv3  5140  prnmaxl  6471  prnminu  6472  elabgft1  9252  elabgf2  9254  bj-axemptylem  9347  bj-notbi  9380  bj-inf2vn  9434  bj-inf2vn2  9435  bj-nn0sucALT  9438
 Copyright terms: Public domain W3C validator