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

Theorem bi2 128
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
bi2  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )

Proof of Theorem bi2
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 )
) )
32simprd 112 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
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  ax-ia2 105
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bicom1  129  pm5.74  177  bi3ant  222  pm5.32d  438  nbn2  646  pm4.72  770  con4biddc  788  con1biimdc  801  bijadc  810  pclem6  1306  exbir  1366  simplbi2comg  1373  albi  1398  exbi  1536  equsexd  1659  cbv2h  1676  sbiedh  1712  ceqsalt  2634  spcegft  2686  elab3gf  2751  euind  2788  reu6  2790  reuind  2804  sbciegft  2853  iota4  4935  fv3  5249  algcvgblem  10638  bj-notbi  10983  bj-inf2vnlem1  11032
  Copyright terms: Public domain W3C validator