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

Theorem imbi2 336
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 328 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  relexpindlem  13600  relexpind  13601  ifpbi2  36654  ifpbi3  36655  3impexpbicom  37530  sbcim2g  37593  3impexpbicomVD  37938  sbcim2gVD  37957  csbeq2gVD  37974  con5VD  37982  hbexgVD  37988  ax6e2ndeqVD  37991  2sb5ndVD  37992  ax6e2ndeqALT  38013  2sb5ndALT  38014
  Copyright terms: Public domain W3C validator