Theorem pm5.74ri 274

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

Step	Hyp	Ref	Expression
1		pm5.74ri.1	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
2		pm5.74 272	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
3	1, 2	mpbir 233	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitrd  281  bibi2d  345  tbt  372  cbvaldvaw  2044  sbiedvw  2103  sbiedw  2331  sbiedwOLD  2332  cbval2vOLD  2363  cbval2OLD  2432  sbied  2544  sbco2d  2553  sbiedALT  2613  2mos  2733  cbvraldva2  3459  cbvrexdva2OLD  3461  axgroth6  10253  isprm2  16029  ufileu  22530