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

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

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  2045  sbiedvw  2101  sbiedw  2323  sbiedwOLD  2324  cbval2vOLD  2353  cbval2OLD  2422  sbied  2522  sbco2d  2531  sbiedALT  2590  2mos  2711  cbvraldva2  3403  cbvrexdva2OLD  3405  axgroth6  10239  isprm2  16016  ufileu  22524