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 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi2d  343  imim21b  399  pm5.74da  815  sbiedvw  2132  sbiedw  2351  dvelimdf  2483  sbied  2537  csbie2df  4400  dfiin2g  4991  oneqmini  6403  tfindsg  7845  findsg  7882  brecop  8796  dom2lem  8977  indpi  10880  nn0ind-raph  12687  sgn3da  15128  cncls2  23391  ismbl2  25647  voliunlem3  25672  mdbr2  32557  dmdbr2  32564  mdsl2i  32583  mdsl2bi  32584  wl-dral1d  38046  wl-equsald  38054  wl-equsaldv  38055  cvlsupr3  39980  cdleme32fva  41073  cdlemk33N  41545  cdlemk34  41546  ralbidar  45018  logic1  49420  tfis2d  50309