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

Theorem bi1 115
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
bi1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )

Proof of Theorem bi1
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 )
) )
32simpld 109 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
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
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biimpi  117  bicom1  126  biimpd  136  ibd  171  pm5.74  172  bi3ant  217  pm5.501  237  pm5.32d  431  pm5.19  632  con4biddc  765  con1biimdc  778  bijadc  787  pclem6  1281  albi  1373  exbi  1511  equsexd  1633  cbv2h  1650  sbiedh  1686  eumo0  1947  ceqsalt  2597  vtoclgft  2621  spcgft  2647  pm13.183  2703  reu6  2752  reu3  2753  sbciegft  2815  fv3  5224  prnmaxl  6643  prnminu  6644  elabgft1  10276  elabgf2  10278  bj-axemptylem  10371  bj-notbi  10404  bj-inf2vn  10458  bj-inf2vn2  10459  bj-nn0sucALT  10462
  Copyright terms: Public domain W3C validator