Theorem syl2and 610

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 607	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 605	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  anim12d  611  ax7  2023  dffi3  8879  cflim2  9674  axpre-sup  10580  xle2add  12640  fzen  12919  rpmulgcd2  15990  pcqmul  16180  initoeu1  17263  termoeu1  17270  plttr  17572  pospo  17575  lublecllem  17590  latjlej12  17669  latmlem12  17685  cygablOLD  19004  hausnei2  21958  uncmp  22008  itgsubst  24652  dvdsmulf1o  25779  2sqlem8a  26009  axcontlem9  26766  uspgr2wlkeq  27435  shintcli  29112  cvntr  30075  cdj3i  30224  f1resrcmplf1dlem  32469  satffunlem  32761  bj-bary1  34726  heicant  35092  itg2addnc  35111  dihmeetlem1N  38586  fmtnofac2lem  44085  2itscp  45195