Theorem pm5.74d 275

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 272	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3	1, 2	sylib 220	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi2d  343  imim21b  397  pm5.74da  802  sbiedvw  2104  sbiedw  2332  sbiedwOLD  2333  cbval2vOLD  2364  cbval2OLD  2433  dvelimdf  2471  sbied  2545  sbiedALT  2614  2mos  2734  cbvraldva2  3458  cbvrexdva2OLD  3460  csbie2df  4394  dfiin2g  4959  oneqmini  6244  tfindsg  7577  findsg  7611  brecop  8392  dom2lem  8551  indpi  10331  nn0ind-raph  12085  cncls2  21883  ismbl2  24130  voliunlem3  24155  mdbr2  30075  dmdbr2  30082  mdsl2i  30101  mdsl2bi  30102  sgn3da  31801  wl-dral1d  34773  wl-equsald  34781  cvlsupr3  36482  cdleme32fva  37575  cdlemk33N  38047  cdlemk34  38048  ralbidar  40784  tfis2d  44790