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  341  imim21b  395  pm5.74da  801  sbiedvw  2096  sbiedw  2310  cbval2vOLD  2341  dvelimdf  2449  sbied  2507  2mos  2651  cbvraldva2  3392  csbie2df  4374  dfiin2g  4962  oneqmini  6317  tfindsg  7707  findsg  7746  brecop  8599  dom2lem  8780  indpi  10663  nn0ind-raph  12420  cncls2  22424  ismbl2  24691  voliunlem3  24716  mdbr2  30658  dmdbr2  30665  mdsl2i  30684  mdsl2bi  30685  sgn3da  32508  wl-dral1d  35690  wl-equsald  35698  cvlsupr3  37358  cdleme32fva  38451  cdlemk33N  38923  cdlemk34  38924  ralbidar  42063  logic1  46136  tfis2d  46386