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:  con3ALT  1084  relexpindlem  14774  relexpind  14775  ifpbi2  41074  ifpbi3  41075  3impexpbicom  42099  sbcim2g  42158  3impexpbicomVD  42477  sbcim2gVD  42495  csbeq2gVD  42512  con5VD  42520  hbexgVD  42526  ax6e2ndeqVD  42529  2sb5ndVD  42530  ax6e2ndeqALT  42551  2sb5ndALT  42552
  Copyright terms: Public domain W3C validator