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  14007  relexpind  14008  ifpbi2  38334  ifpbi3  38335  3impexpbicom  39207  sbcim2g  39270  3impexpbicomVD  39611  sbcim2gVD  39630  csbeq2gVD  39647  con5VD  39655  hbexgVD  39661  ax6e2ndeqVD  39664  2sb5ndVD  39665  ax6e2ndeqALT  39686  2sb5ndALT  39687
  Copyright terms: Public domain W3C validator