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  2095  sbiedw  2316  dvelimdf  2453  sbied  2507  2mosOLD  2649  cbvraldva2  3327  csbie2df  4418  dfiin2g  5008  oneqmini  6405  tfindsg  7856  findsg  7893  brecop  8824  dom2lem  9006  indpi  10921  nn0ind-raph  12693  cncls2  23211  ismbl2  25480  voliunlem3  25505  mdbr2  32277  dmdbr2  32284  mdsl2i  32303  mdsl2bi  32304  sgn3da  32813  wl-dral1d  37549  wl-equsald  37557  wl-equsaldv  37558  cvlsupr3  39362  cdleme32fva  40456  cdlemk33N  40928  cdlemk34  40929  ralbidar  44469  logic1  48770  tfis2d  49544