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  804  sbiedvw  2101  sbiedw  2322  dvelimdf  2454  sbied  2508  2mosOLD  2651  csbie2df  4384  dfiin2g  4974  oneqmini  6370  tfindsg  7805  findsg  7841  brecop  8750  dom2lem  8932  indpi  10821  nn0ind-raph  12620  cncls2  23248  ismbl2  25504  voliunlem3  25529  mdbr2  32382  dmdbr2  32389  mdsl2i  32408  mdsl2bi  32409  sgn3da  32922  wl-dral1d  37870  wl-equsald  37878  wl-equsaldv  37879  cvlsupr3  39804  cdleme32fva  40897  cdlemk33N  41369  cdlemk34  41370  ralbidar  44889  logic1  49278  tfis2d  50167