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

Theorem imbi2 337
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 329 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  relexpindlem  14022  relexpind  14023  ifpbi2  38331  ifpbi3  38332  3impexpbicom  39205  sbcim2g  39268  3impexpbicomVD  39609  sbcim2gVD  39628  csbeq2gVD  39645  con5VD  39653  hbexgVD  39659  ax6e2ndeqVD  39662  2sb5ndVD  39663  ax6e2ndeqALT  39684  2sb5ndALT  39685
  Copyright terms: Public domain W3C validator