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

Theorem imbi2 348
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 340 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  imbibi  391  con3ALT  1084  axpr  5433  relexpindlem  15099  relexpind  15100  unielss  43207  ifpbi2  43457  ifpbi3  43458  3impexpbicom  44477  sbcim2g  44536  3impexpbicomVD  44855  sbcim2gVD  44873  csbeq2gVD  44890  con5VD  44898  hbexgVD  44904  ax6e2ndeqVD  44907  2sb5ndVD  44908  ax6e2ndeqALT  44929  2sb5ndALT  44930
  Copyright terms: Public domain W3C validator