Theorem pm5.74d 265

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imbi2d  333  imim21b  386  pm5.74da  791  cbval2OLD  2344  dvelimdf  2383  sbied  2467  sbiedALT  2538  2mos  2675  cbvraldva2  3381  cbvrexdva2OLD  3383  dfiin2g  4821  oneqmini  6074  tfindsg  7385  findsg  7418  brecop  8182  dom2lem  8338  indpi  10119  nn0ind-raph  11888  cncls2  21575  ismbl2  23821  voliunlem3  23846  mdbr2  29844  dmdbr2  29851  mdsl2i  29870  mdsl2bi  29871  sgn3da  31402  bj-cbval2v  33522  wl-dral1d  34149  wl-equsald  34157  cvlsupr3  35873  cdleme32fva  36966  cdlemk33N  37438  cdlemk34  37439  ralbidar  40140  tfis2d  44090