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

Theorem imbi2 316
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 21 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21imbi2d 309 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  ->  ph )  <->  ( ch  ->  ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  3impexpbicom  1363  relexpindlem  23207  relexpind  23208  sbcim2g  27092  3impexpbicomVD  27420  sbcim2gVD  27438  csbeq2gVD  27455  con5VD  27463  hbexgVD  27469  a9e2ndeqVD  27472  2sb5ndVD  27473  a9e2ndeqALT  27495  2sb5ndALT  27496
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator