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

Theorem pm5.74ri 275
Description: Distribution of implication over biconditional (reverse inference form). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.74ri.1 ((𝜑𝜓) ↔ (𝜑𝜒))
Assertion
Ref Expression
pm5.74ri (𝜑 → (𝜓𝜒))

Proof of Theorem pm5.74ri
StepHypRef Expression
1 pm5.74ri.1 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
2 pm5.74 273 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbir 234 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:  bitrd  282  bibi2d  346  tbt  373  cbvaldvaw  2050  sbiedvw  2104  sbiedw  2317  sbiedwOLD  2318  cbval2vOLD  2346  sbied  2507  sbco2d  2516  2mos  2652  cbvraldva2  3358  axgroth6  10330  isprm2  16125  ufileu  22672
  Copyright terms: Public domain W3C validator