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  655  con4biddc  788  con1biimdc  801  bijadc  810  pclem6  1306  albi  1398  exbi  1536  equsexd  1659  cbv2h  1676  sbiedh  1712  eumo0  1974  ceqsalt  2634  vtoclgft  2658  spcgft  2684  pm13.183  2740  reu6  2790  reu3  2791  sbciegft  2853  ddifstab  3114  fv3  5249  prnmaxl  6792  prnminu  6793  elabgft1  10848  elabgf2  10850  bj-axemptylem  10950  bj-notbi  10983  bj-inf2vn  11036  bj-inf2vn2  11037  bj-nn0sucALT  11040
  Copyright terms: Public domain W3C validator