Theorem syl3an3 1183

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syl3an3.1	⊢ (𝜑 → 𝜃)
syl3an3.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2	1	3anim3i 1172	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 18	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  3adant3l  1199  3adant3r  1200  syl3an3b  1432  syl3an3br  1435  disji  5087  ovmpox  7574  ovmpoga  7575  wrecseq123  8335  tz7.48lem  8454  dif1en  9181  domtrfil  9211  ssdomfi2  9216  domnsymfi  9219  sdomdomtrfi  9220  domsdomtrfi  9221  phplem2  9224  php  9226  php3  9228  findcard3  9278  unbnn2  9293  axdc3lem4  10535  axdclem2  10602  gruiin  10899  gruen  10901  divass  11996  ltmul2  12172  ind0  12334  xleadd1  13389  xltadd2  13391  xlemul1  13424  xltmul2  13427  elfzo  13799  modcyc2  14051  faclbnd5  14446  swrdrevpfx  14923  relexprel  15198  subcn2  15768  mulcn2  15769  ndvdsp1  16587  gcddiv  16730  dvdsexpnn  16746  lcmneg  16784  lubel  18694  mndpfsupp  18967  gsumccatsn  19045  mulgaddcom  19314  oddvdsi  19768  odcong  19769  odeq  19770  efgsp1  19957  lspsnss  21271  rnglidlrng  21541  lindsmm2  22141  mulmarep1el  22893  mdetunilem4  22936  iuncld  23369  neips  23437  opnneip  23443  comppfsc  23857  hmeof1o2  24088  ordthmeo  24127  ufinffr  24254  elfm3  24275  utop3cls  24576  blcntrps  24737  blcntr  24738  neibl  24826  blnei  24827  metss  24833  stdbdmetval  24839  prdsms  24856  blval2  24887  lmmbr  25585  lmmbr2  25586  iscau2  25604  bcthlem1  25651  bcthlem3  25653  bcthlem4  25654  dvn2bss  26256  dvfsumrlim  26357  dvfsumrlim2  26358  cxpexpz  27001  cxpsub  27016  cxpcom  27073  relogbzexp  27110  ltsubs1  28468  1ewlk  30712  1pthon2ve  30761  upgr4cycl4dv4e  30792  konigsbergssiedgwpr  30856  dlwwlknondlwlknonf1o  30972  hvaddsub12  31646  hvaddsubass  31649  hvsubdistr1  31657  hvsubcan  31682  hhssnv  31872  spanunsni  32187  homco1  32409  homulass  32410  hoadddir  32412  hosubdi  32416  hoaddsubass  32423  hosubsub4  32426  lnopmi  32608  adjlnop  32694  mdsymlem5  33015  disjif  33220  disjif2  33223  sigaclfu  34798  signstfvc  35250  bnj544  35571  bnj561  35580  bnj562  35581  bnj594  35589  fineqvnttrclselem3  35848  satfvsuc  36213  satfvsucsuc  36217  clsint2  37210  weiunso  37347  weiunwe  37350  ftc1anclem6  38710  isbnd2  38811  blbnd  38815  isdrngo2  38986  atnem0  40469  hlrelat5N  40552  ltrnel  41290  ltrnat  41291  ltrncnvat  41292  nnproddivdvdsd  43144  jm2.22  44096  jm2.23  44097  dvconstbi  45412  eelT11  45783  eelT12  45785  eelTT1  45786  eelT01  45787  eel0T1  45788  liminfvalxr  46887  grlimprclnbgr  49188  rmfsupp  49579  scmfsupp  49581  dignn0flhalflem2  49822  rrx2vlinest  49947  rrx2linesl  49949