Theorem syl2and 620

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d  621  ax7  2049  f1resrcmplf1dlem  7266  dffi3  9401  cflim2  10313  axpre-sup  11226  xle2add  13359  fzen  13643  rpmulgcd2  16794  pcqmul  16993  sbcie2s  17301  initoeu1  18148  termoeu1  18155  plttr  18476  pospo  18479  lublecllem  18494  latjlej12  18591  latmlem12  18607  hausnei2  23633  uncmp  23683  itgsubst  26331  mpodvdsmulf1o  27485  dvdsmulf1o  27487  2sqlem8a  27716  precsexlem10  28536  axcontlem9  29484  uspgr2wlkeq  30160  shintcli  31865  cvntr  32828  cdj3i  32977  satffunlem  36087  bj-bary1  38153  heicant  38493  itg2addnc  38512  findcard4  38552  dihmeetlem1N  42267  modelaxreplem1  45905  fmtnofac2lem  48575  2itscp  49815  mofsn  49876