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

Theorem bi1 117
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 116 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 110 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
32simpld 111 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimpi  119  bicom1  130  biimpd  143  ibd  177  pm5.74  178  bi3ant  223  pm5.501  243  pm5.32d  445  notbi  640  pm5.19  680  con4biddc  827  con1biimdc  843  bijadc  852  pclem6  1337  albi  1429  exbi  1568  equsexd  1692  cbv2h  1709  sbiedh  1745  eumo0  2008  ceqsalt  2686  vtoclgft  2710  spcgft  2737  pm13.183  2796  reu6  2846  reu3  2847  sbciegft  2911  ddifstab  3178  exmidsssnc  4096  fv3  5412  prnmaxl  7264  prnminu  7265  elabgft1  12912  elabgf2  12914  bj-axemptylem  13017  bj-inf2vn  13099  bj-inf2vn2  13100  bj-nn0sucALT  13103
  Copyright terms: Public domain W3C validator