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  339  imim21b  393  pm5.74da  802  sbiedvw  2089  sbiedw  2305  dvelimdf  2443  sbied  2497  2mosOLD  2639  cbvraldva2  3332  csbie2df  4437  dfiin2g  5032  oneqmini  6420  tfindsg  7863  findsg  7902  brecop  8831  dom2lem  9015  indpi  10941  nn0ind-raph  12708  cncls2  23265  ismbl2  25544  voliunlem3  25569  mdbr2  32226  dmdbr2  32233  mdsl2i  32252  mdsl2bi  32253  sgn3da  34388  wl-dral1d  37239  wl-equsald  37247  wl-equsaldv  37248  cvlsupr3  39055  cdleme32fva  40149  cdlemk33N  40621  cdlemk34  40622  ralbidar  44156  logic1  48214  tfis2d  48462