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

Theorem imbi2 339
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 331 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  relexpindlem  14020  relexpind  14021  ifpbi2  38305  ifpbi3  38306  3impexpbicom  39177  sbcim2g  39240  3impexpbicomVD  39580  sbcim2gVD  39599  csbeq2gVD  39616  con5VD  39624  hbexgVD  39630  ax6e2ndeqVD  39633  2sb5ndVD  39634  ax6e2ndeqALT  39655  2sb5ndALT  39656
  Copyright terms: Public domain W3C validator