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  5099  ovmpox  7576  ovmpoga  7577  wrecseq123  8319  dif1en  9156  domtrfil  9186  ssdomfi2  9191  domnsymfi  9194  sdomdomtrfi  9195  domsdomtrfi  9196  phplem2  9199  php  9201  php3  9203  findcard3  9253  unbnn2  9267  axdc3lem4  10455  axdclem2  10522  gruiin  10813  gruen  10815  divass  11908  ltmul2  12084  ind0  12246  xleadd1  13299  xltadd2  13301  xlemul1  13334  xltmul2  13337  elfzo  13708  modcyc2  13960  faclbnd5  14354  swrdrevpfx  14830  relexprel  15102  subcn2  15672  mulcn2  15673  ndvdsp1  16494  gcddiv  16634  lcmneg  16686  lubel  18595  mndpfsupp  18856  gsumccatsn  18933  mulgaddcom  19195  oddvdsi  19649  odcong  19650  odeq  19651  efgsp1  19838  lspsnss  21148  rnglidlrng  21418  lindsmm2  22016  mulmarep1el  22766  mdetunilem4  22809  iuncld  23239  neips  23307  opnneip  23313  comppfsc  23726  hmeof1o2  23957  ordthmeo  23996  ufinffr  24123  elfm3  24144  utop3cls  24445  blcntrps  24606  blcntr  24607  neibl  24695  blnei  24696  metss  24702  stdbdmetval  24708  prdsms  24725  blval2  24756  lmmbr  25454  lmmbr2  25455  iscau2  25473  bcthlem1  25520  bcthlem3  25522  bcthlem4  25523  dvn2bss  26126  dvfsumrlim  26227  dvfsumrlim2  26228  cxpexpz  26869  cxpsub  26884  cxpcom  26941  relogbzexp  26978  ltsubs1  28306  1ewlk  30503  1pthon2ve  30542  upgr4cycl4dv4e  30573  konigsbergssiedgwpr  30637  dlwwlknondlwlknonf1o  30753  hvaddsub12  31427  hvaddsubass  31430  hvsubdistr1  31438  hvsubcan  31463  hhssnv  31653  spanunsni  31968  homco1  32190  homulass  32191  hoadddir  32193  hosubdi  32197  hoaddsubass  32204  hosubsub4  32207  lnopmi  32389  adjlnop  32475  mdsymlem5  32796  disjif  32960  disjif2  32963  sigaclfu  34540  signstfvc  34992  bnj544  35313  bnj561  35322  bnj562  35323  bnj594  35331  fineqvnttrclselem3  35559  satfvsuc  35873  satfvsucsuc  35877  clsint2  36880  weiunso  37017  weiunwe  37020  ftc1anclem6  38389  isbnd2  38474  blbnd  38478  isdrngo2  38649  atnem0  40132  hlrelat5N  40215  ltrnel  40953  ltrnat  40954  ltrncnvat  40955  nnproddivdvdsd  42807  dvdsexpnn  43134  jm2.22  43762  jm2.23  43763  dvconstbi  45084  eelT11  45455  eelT12  45457  eelTT1  45458  eelT01  45459  eel0T1  45460  liminfvalxr  46537  grlimprclnbgr  48801  rmfsupp  49193  scmfsupp  49195  dignn0flhalflem2  49436  rrx2vlinest  49561  rrx2linesl  49563