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  2321  dvelimdf  2453  sbied  2507  2mosOLD  2650  cbvraldva2  3318  csbie2df  4395  dfiin2g  4986  oneqmini  6370  tfindsg  7803  findsg  7839  brecop  8747  dom2lem  8929  indpi  10818  nn0ind-raph  12592  cncls2  23217  ismbl2  25484  voliunlem3  25509  mdbr2  32371  dmdbr2  32378  mdsl2i  32397  mdsl2bi  32398  sgn3da  32915  wl-dral1d  37732  wl-equsald  37740  wl-equsaldv  37741  cvlsupr3  39600  cdleme32fva  40693  cdlemk33N  41165  cdlemk34  41166  ralbidar  44681  logic1  49032  tfis2d  49921