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

Theorem imbi2 350
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 342 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  con3ALT  1076  relexpindlem  14410  relexpind  14411  ifpbi2  39710  ifpbi3  39711  3impexpbicom  40690  sbcim2g  40749  3impexpbicomVD  41068  sbcim2gVD  41086  csbeq2gVD  41103  con5VD  41111  hbexgVD  41117  ax6e2ndeqVD  41120  2sb5ndVD  41121  ax6e2ndeqALT  41142  2sb5ndALT  41143
  Copyright terms: Public domain W3C validator