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 23 . 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  13105  relexpind  13106  ifpbi2  35809  ifpbi3  35810  3impexpbicom  36471  sbcim2g  36536  3impexpbicomVD  36893  sbcim2gVD  36912  csbeq2gVD  36929  con5VD  36937  hbexgVD  36943  ax6e2ndeqVD  36946  2sb5ndVD  36947  ax6e2ndeqALT  36968  2sb5ndALT  36969
  Copyright terms: Public domain W3C validator