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

Theorem imbi2 352
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 344 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  con3ALT  1086  relexpindlem  14524  relexpind  14525  ifpbi2  40668  ifpbi3  40669  3impexpbicom  41677  sbcim2g  41736  3impexpbicomVD  42055  sbcim2gVD  42073  csbeq2gVD  42090  con5VD  42098  hbexgVD  42104  ax6e2ndeqVD  42107  2sb5ndVD  42108  ax6e2ndeqALT  42129  2sb5ndALT  42130
  Copyright terms: Public domain W3C validator