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

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

Proof of Theorem biimpr
StepHypRef Expression
1 df-bi 117 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 111 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
32simprd 114 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bicom1  131  pm5.74  179  bi3ant  224  pm5.32d  450  notbi  666  nbn2  697  pm4.72  827  con4biddc  857  con1biimdc  873  bijadc  882  pclem6  1374  exbir  1436  simplbi2comg  1443  albi  1468  exbi  1604  equsexd  1729  cbv2h  1748  cbv2w  1750  sbiedh  1787  ceqsalt  2764  spcegft  2817  elab3gf  2888  euind  2925  reu6  2927  reuind  2943  sbciegft  2994  iota4  5197  fv3  5539  algcvgblem  12049  bj-inf2vnlem1  14725
  Copyright terms: Public domain W3C validator