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  2133  sbiedw  2352  dvelimdf  2484  sbied  2538  csbie2df  4411  dfiin2g  5000  oneqmini  6421  tfindsg  7866  findsg  7903  brecop  8817  dom2lem  8998  indpi  10910  nn0ind-raph  12714  sgn3da  15164  cncls2  23467  ismbl2  25723  voliunlem3  25748  mdbr2  32685  dmdbr2  32692  mdsl2i  32711  mdsl2bi  32712  wl-dral1d  38227  wl-equsald  38235  wl-equsaldv  38236  cvlsupr3  40159  cdleme32fva  41252  cdlemk33N  41724  cdlemk34  41725  ralbidar  45195  logic1  49610  tfis2d  50499