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

Theorem bi2 125
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
bi2  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )

Proof of Theorem bi2
StepHypRef Expression
1 df-bi 114 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 108 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
32simprd 111 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bicom1  126  pm5.74  172  bi3ant  217  pm5.32d  431  nbn2  623  pm4.72  747  con4biddc  765  con1biimdc  778  bijadc  787  pclem6  1281  exbir  1341  simplbi2comg  1348  albi  1373  exbi  1511  equsexd  1633  cbv2h  1650  sbiedh  1686  ceqsalt  2597  spcegft  2649  elab3gf  2714  euind  2750  reu6  2752  reuind  2766  sbciegft  2815  iota4  4912  fv3  5224  algcvgblem  10243  bj-notbi  10404  bj-inf2vnlem1  10454
  Copyright terms: Public domain W3C validator