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  399  pm5.74da  815  sbiedvw  2129  sbiedw  2348  dvelimdf  2480  sbied  2534  csbie2df  4407  dfiin2g  4994  oneqmini  6414  tfindsg  7855  findsg  7892  brecop  8806  dom2lem  8987  indpi  10898  nn0ind-raph  12702  sgn3da  15145  cncls2  23441  ismbl2  25697  voliunlem3  25722  mdbr2  32659  dmdbr2  32666  mdsl2i  32685  mdsl2bi  32686  wl-dral1d  38214  wl-equsald  38222  wl-equsaldv  38223  cvlsupr3  40146  cdleme32fva  41239  cdlemk33N  41711  cdlemk34  41712  ralbidar  45182  logic1  49597  tfis2d  50486