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 195
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 196
This theorem is referenced by:  relexpindlem  13651  relexpind  13652  ifpbi2  36830  ifpbi3  36831  3impexpbicom  37706  sbcim2g  37769  3impexpbicomVD  38114  sbcim2gVD  38133  csbeq2gVD  38150  con5VD  38158  hbexgVD  38164  ax6e2ndeqVD  38167  2sb5ndVD  38168  ax6e2ndeqALT  38189  2sb5ndALT  38190
  Copyright terms: Public domain W3C validator