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  2015  dffi3  9441  cflim2  10275  axpre-sup  11181  xle2add  13273  fzen  13556  rpmulgcd2  16673  pcqmul  16871  sbcie2s  17178  initoeu1  18022  termoeu1  18029  plttr  18350  pospo  18353  lublecllem  18368  latjlej12  18463  latmlem12  18479  hausnei2  23289  uncmp  23339  itgsubst  26006  mpodvdsmulf1o  27154  dvdsmulf1o  27156  2sqlem8a  27386  precsexlem10  28157  axcontlem9  28897  uspgr2wlkeq  29572  shintcli  31256  cvntr  32219  cdj3i  32368  f1resrcmplf1dlem  35063  satffunlem  35369  bj-bary1  37276  heicant  37625  itg2addnc  37644  dihmeetlem1N  41255  modelaxreplem1  44951  fmtnofac2lem  47530  2itscp  48709  mofsn  48770