Theorem pm5.74d 276

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi2d  343  imim21b  400  pm5.74da  816  sbiedvw  2132  sbiedw  2347  dvelimdf  2479  sbied  2533  csbie2df  4401  dfiin2g  4989  oneqmini  6409  tfindsg  7861  findsg  7898  brecop  8815  dom2lem  9003  indpi  10973  nn0ind-raph  12780  sgn3da  15234  cncls2  23571  ismbl2  25828  voliunlem3  25853  mdbr2  32880  dmdbr2  32887  mdsl2i  32906  mdsl2bi  32907  wl-dral1d  38431  wl-equsald  38439  wl-equsaldv  38440  cvlsupr3  40369  cdleme32fva  41462  cdlemk33N  41934  cdlemk34  41935  ralbidar  45387  imbi12d2  49845  tfis2d  50731