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

Theorem imbi2 315
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 20 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21imbi2d 308 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  ->  ph )  <->  ( ch  ->  ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3impexpbicom  1376  relexpindlem  25127  relexpind  25128  sbcim2g  28478  3impexpbicomVD  28823  sbcim2gVD  28841  csbeq2gVD  28858  con5VD  28866  hbexgVD  28872  a9e2ndeqVD  28875  2sb5ndVD  28876  a9e2ndeqALT  28898  2sb5ndALT  28899
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 178
  Copyright terms: Public domain W3C validator