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  2098  sbiedw  2317  dvelimdf  2449  sbied  2503  2mosOLD  2645  cbvraldva2  3314  csbie2df  4393  dfiin2g  4981  oneqmini  6359  tfindsg  7791  findsg  7827  brecop  8734  dom2lem  8914  indpi  10795  nn0ind-raph  12570  cncls2  23186  ismbl2  25453  voliunlem3  25478  mdbr2  32271  dmdbr2  32278  mdsl2i  32297  mdsl2bi  32298  sgn3da  32812  wl-dral1d  37564  wl-equsald  37572  wl-equsaldv  37573  cvlsupr3  39382  cdleme32fva  40475  cdlemk33N  40947  cdlemk34  40948  ralbidar  44476  logic1  48821  tfis2d  49711