Theorem pm5.74d 272

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi2d  340  imim21b  395  pm5.74da  802  sbiedvw  2096  sbiedw  2310  dvelimdf  2448  sbied  2506  2mos  2650  cbvraldva2  3321  csbie2df  4398  dfiin2g  4990  oneqmini  6367  tfindsg  7789  findsg  7828  brecop  8707  dom2lem  8890  indpi  10801  nn0ind-raph  12561  cncls2  22576  ismbl2  24843  voliunlem3  24868  mdbr2  31067  dmdbr2  31074  mdsl2i  31093  mdsl2bi  31094  sgn3da  32953  wl-dral1d  35928  wl-equsald  35936  cvlsupr3  37744  cdleme32fva  38838  cdlemk33N  39310  cdlemk34  39311  ralbidar  42636  logic1  46777  tfis2d  47026