Theorem syl2and 606

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anim12d  607  ax7  2011  dffi3  9454  cflim2  10286  axpre-sup  11192  xle2add  13270  fzen  13550  rpmulgcd2  16626  pcqmul  16821  sbcie2s  17129  initoeu1  17999  termoeu1  18006  plttr  18333  pospo  18336  lublecllem  18351  latjlej12  18446  latmlem12  18462  hausnei2  23287  uncmp  23337  itgsubst  26014  mpodvdsmulf1o  27156  dvdsmulf1o  27158  2sqlem8a  27388  precsexlem10  28148  axcontlem9  28839  uspgr2wlkeq  29516  shintcli  31195  cvntr  32158  cdj3i  32307  f1resrcmplf1dlem  34779  satffunlem  35081  bj-bary1  36861  heicant  37198  itg2addnc  37217  dihmeetlem1N  40832  fmtnofac2lem  46971  2itscp  47966  mofsn  48008