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

Theorem imbi2 325
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 22 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21imbi2d 317 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  ->  ph )  <->  ( ch  ->  ps )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  relexpindlem  13065  relexpind  13066  ifpbi2  36023  ifpbi3  36024  3impexpbicom  36747  sbcim2g  36812  3impexpbicomVD  37169  sbcim2gVD  37188  csbeq2gVD  37205  con5VD  37213  hbexgVD  37219  ax6e2ndeqVD  37222  2sb5ndVD  37223  ax6e2ndeqALT  37244  2sb5ndALT  37245
  Copyright terms: Public domain W3C validator