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

Theorem imbi2 349
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 341 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  imbibi  393  con3ALT  1086  relexpindlem  15007  relexpind  15008  unielss  41953  ifpbi2  42204  ifpbi3  42205  3impexpbicom  43226  sbcim2g  43285  3impexpbicomVD  43604  sbcim2gVD  43622  csbeq2gVD  43639  con5VD  43647  hbexgVD  43653  ax6e2ndeqVD  43656  2sb5ndVD  43657  ax6e2ndeqALT  43678  2sb5ndALT  43679
  Copyright terms: Public domain W3C validator