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  2048  f1resrcmplf1dlem  7278  dffi3  9424  cflim2  10342  axpre-sup  11255  xle2add  13390  fzen  13675  rpmulgcd2  16832  pcqmul  17032  sbcie2s  17340  initoeu1  18187  termoeu1  18194  plttr  18515  pospo  18518  lublecllem  18533  latjlej12  18630  latmlem12  18646  hausnei2  23672  uncmp  23722  itgsubst  26370  mpodvdsmulf1o  27522  dvdsmulf1o  27524  2sqlem8a  27753  precsexlem10  28603  axcontlem9  29551  uspgr2wlkeq  30227  shintcli  31932  cvntr  32895  cdj3i  33044  satffunlem  36235  bj-bary1  38309  heicant  38649  itg2addnc  38668  findcard4  38708  dihmeetlem1N  42423  modelaxreplem1  46044  fmtnofac2lem  48729  2itscp  49969  mofsn  50030