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  2132  sbiedw  2348  dvelimdf  2480  sbied  2534  csbie2df  4404  dfiin2g  4993  oneqmini  6415  tfindsg  7861  findsg  7898  brecop  8814  dom2lem  9002  indpi  10920  nn0ind-raph  12725  sgn3da  15178  cncls2  23504  ismbl2  25761  voliunlem3  25786  mdbr2  32785  dmdbr2  32792  mdsl2i  32811  mdsl2bi  32812  wl-dral1d  38302  wl-equsald  38310  wl-equsaldv  38311  cvlsupr3  40225  cdleme32fva  41318  cdlemk33N  41790  cdlemk34  41791  ralbidar  45276  logic1  49727  tfis2d  50614