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  443  notbi  638  pm5.19  678  con4biddc  825  con1biimdc  841  bijadc  850  pclem6  1335  albi  1427  exbi  1566  equsexd  1690  cbv2h  1707  sbiedh  1743  eumo0  2006  ceqsalt  2684  vtoclgft  2708  spcgft  2735  pm13.183  2794  reu6  2844  reu3  2845  sbciegft  2909  ddifstab  3176  exmidsssnc  4094  fv3  5410  prnmaxl  7260  prnminu  7261  elabgft1  12819  elabgf2  12821  bj-axemptylem  12924  bj-inf2vn  13006  bj-inf2vn2  13007  bj-nn0sucALT  13010
  Copyright terms: Public domain W3C validator