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 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 400

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

This theorem is referenced by:  anim12d  620  ax7  2044  dffi3  9390  cflim2  10246  axpre-sup  11153  xle2add  13284  fzen  13568  rpmulgcd2  16713  pcqmul  16912  sbcie2s  17220  initoeu1  18067  termoeu1  18074  plttr  18395  pospo  18398  lublecllem  18413  latjlej12  18510  latmlem12  18526  hausnei2  23489  uncmp  23539  itgsubst  26187  mpodvdsmulf1o  27334  dvdsmulf1o  27336  2sqlem8a  27565  precsexlem10  28385  axcontlem9  29288  uspgr2wlkeq  29961  shintcli  31647  cvntr  32610  cdj3i  32759  f1resrcmplf1dlem  35440  satffunlem  35859  bj-bary1  37922  heicant  38272  itg2addnc  38291  dihmeetlem1N  42032  modelaxreplem1  45657  fmtnofac2lem  48287  2itscp  49528  mofsn  49589