Theorem syl2and 608

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anim12d  609  ax7  2017  dffi3  9334  cflim2  10173  axpre-sup  11080  xle2add  13174  fzen  13457  rpmulgcd2  16583  pcqmul  16781  sbcie2s  17088  initoeu1  17935  termoeu1  17942  plttr  18263  pospo  18266  lublecllem  18281  latjlej12  18378  latmlem12  18394  hausnei2  23297  uncmp  23347  itgsubst  26012  mpodvdsmulf1o  27160  dvdsmulf1o  27162  2sqlem8a  27392  precsexlem10  28212  axcontlem9  29045  uspgr2wlkeq  29719  shintcli  31404  cvntr  32367  cdj3i  32516  f1resrcmplf1dlem  35242  satffunlem  35595  bj-bary1  37517  heicant  37856  itg2addnc  37875  dihmeetlem1N  41550  modelaxreplem1  45219  fmtnofac2lem  47814  2itscp  49027  mofsn  49089