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

Theorem bi1 116
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 115 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 109 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
32simpld 110 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimpi  118  bicom1  129  biimpd  142  ibd  176  pm5.74  177  bi3ant  222  pm5.501  242  pm5.32d  438  pm5.19  657  con4biddc  792  con1biimdc  805  bijadc  814  pclem6  1310  albi  1402  exbi  1540  equsexd  1664  cbv2h  1681  sbiedh  1717  eumo0  1979  ceqsalt  2645  vtoclgft  2669  spcgft  2696  pm13.183  2754  reu6  2804  reu3  2805  sbciegft  2869  ddifstab  3132  fv3  5328  prnmaxl  7047  prnminu  7048  elabgft1  11678  elabgf2  11680  bj-axemptylem  11783  bj-notbi  11816  bj-inf2vn  11869  bj-inf2vn2  11870  bj-nn0sucALT  11873
  Copyright terms: Public domain W3C validator