Theorem pm5.74d 275

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.)

Hypothesis

Ref	Expression
pm5.74d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.74d	⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Proof of Theorem pm5.74d

Step	Hyp	Ref	Expression
1		pm5.74d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.74 272	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3	1, 2	sylib 220	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:  imbi2d  342  imim21b  398  pm5.74da  813  sbiedvw  2128  sbiedw  2347  dvelimdf  2479  sbied  2533  csbie2df  4396  dfiin2g  4987  oneqmini  6395  tfindsg  7837  findsg  7874  brecop  8787  dom2lem  8969  indpi  10862  nn0ind-raph  12670  cncls2  23313  ismbl2  25569  voliunlem3  25594  mdbr2  32445  dmdbr2  32452  mdsl2i  32471  mdsl2bi  32472  sgn3da  32986  wl-dral1d  37998  wl-equsald  38006  wl-equsaldv  38007  cvlsupr3  39932  cdleme32fva  41025  cdlemk33N  41497  cdlemk34  41498  ralbidar  44984  logic1  49376  tfis2d  50265