Theorem pm5.74d 273

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 270	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3	1, 2	sylib 218	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi2d  340  imim21b  394  pm5.74da  803  sbiedvw  2100  sbiedw  2319  dvelimdf  2451  sbied  2505  2mosOLD  2647  cbvraldva2  3315  csbie2df  4392  dfiin2g  4981  oneqmini  6364  tfindsg  7797  findsg  7833  brecop  8740  dom2lem  8921  indpi  10805  nn0ind-raph  12579  cncls2  23189  ismbl2  25456  voliunlem3  25481  mdbr2  32278  dmdbr2  32285  mdsl2i  32304  mdsl2bi  32305  sgn3da  32822  wl-dral1d  37596  wl-equsald  37604  wl-equsaldv  37605  cvlsupr3  39463  cdleme32fva  40556  cdlemk33N  41028  cdlemk34  41029  ralbidar  44561  logic1  48915  tfis2d  49805