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  2134  sbiedw  2350  dvelimdf  2481  sbied  2535  csbie2df  4404  dfiin2g  4992  oneqmini  6437  tfindsg  7899  findsg  7936  brecop  8862  dom2lem  9050  indpi  11022  nn0ind-raph  12829  sgn3da  15286  cncls2  23624  ismbl2  25881  voliunlem3  25906  mdbr2  32931  dmdbr2  32938  mdsl2i  32957  mdsl2bi  32958  wl-dral1d  38668  wl-equsald  38676  wl-equsaldv  38677  cvlsupr3  40604  cdleme32fva  41697  cdlemk33N  42169  cdlemk34  42170  ralbidar  45630  imbi12d2  50116  tfis2d  51077