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

Theorem pm5.74ri 273
 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 271 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbir 232 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207 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 208 This theorem is referenced by:  bitrd  280  bibi2d  344  tbt  371  cbvaldvaw  2038  sbiedvw  2097  sbiedw  2326  sbiedwOLD  2327  cbval2vOLD  2358  cbval2OLD  2429  sbied  2543  sbco2d  2552  sbiedALT  2611  2mos  2732  cbvraldva2  3461  cbvrexdva2OLD  3463  axgroth6  10242  isprm2  16018  ufileu  22445
 Copyright terms: Public domain W3C validator