Theorem syl2and 619

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syl2and.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl2and.2	⊢ (𝜑 → (𝜃 → 𝜏))
syl2and.3	⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))

Assertion

Ref	Expression
syl2and	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl2and.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3		syl2and.3	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))
4	2, 3	sylan2d 616	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 614	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

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  df-an 401

This theorem is used by:  anim12d  620  ax7  2045  dffi3  9389  cflim2  10253  axpre-sup  11160  xle2add  13291  fzen  13575  rpmulgcd2  16720  pcqmul  16919  sbcie2s  17227  initoeu1  18074  termoeu1  18081  plttr  18402  pospo  18405  lublecllem  18420  latjlej12  18517  latmlem12  18533  hausnei2  23521  uncmp  23571  itgsubst  26219  mpodvdsmulf1o  27369  dvdsmulf1o  27371  2sqlem8a  27600  precsexlem10  28420  axcontlem9  29333  uspgr2wlkeq  30006  shintcli  31692  cvntr  32655  cdj3i  32804  f1resrcmplf1dlem  35483  satffunlem  35901  bj-bary1  37984  heicant  38334  itg2addnc  38353  dihmeetlem1N  42092  modelaxreplem1  45715  fmtnofac2lem  48348  2itscp  49589  mofsn  49650