MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2 Unicode version

Theorem imbi2 314
Description: Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Assertion
Ref Expression
imbi2  |-  ( (
ph 
<->  ps )  ->  (
( ch  ->  ph )  <->  ( ch  ->  ps )
) )

Proof of Theorem imbi2
StepHypRef Expression
1 id 19 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21imbi2d 307 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  ->  ph )  <->  ( ch  ->  ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3impexpbicom  1357  relexpindlem  24051  relexpind  24052  sbcim2g  28601  3impexpbicomVD  28949  sbcim2gVD  28967  csbeq2gVD  28984  con5VD  28992  hbexgVD  28998  a9e2ndeqVD  29001  2sb5ndVD  29002  a9e2ndeqALT  29024  2sb5ndALT  29025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator