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

Theorem imbi2 348
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 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))

Proof of Theorem imbi2
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21imbi2d 340 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  imbibi  391  con3ALT  1085  axpr  5427  relexpindlem  15102  relexpind  15103  unielss  43230  ifpbi2  43480  ifpbi3  43481  3impexpbicom  44500  sbcim2g  44558  3impexpbicomVD  44877  sbcim2gVD  44895  csbeq2gVD  44912  con5VD  44920  hbexgVD  44926  ax6e2ndeqVD  44929  2sb5ndVD  44930  ax6e2ndeqALT  44951  2sb5ndALT  44952
  Copyright terms: Public domain W3C validator