Theorem syl3an3 1165

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 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3l  1181  3adant3r  1182  syl3an3b  1407  syl3an3br  1410  disji  5080  ovmpox  7506  ovmpoga  7507  wrecseq123  8253  dif1en  9084  dif1enOLD  9086  domtrfil  9116  ssdomfi2  9121  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  phplem2  9129  php  9131  php3  9133  findcard3  9187  unbnn2  9202  axdc3lem4  10366  axdclem2  10433  gruiin  10723  gruen  10725  divass  11815  ltmul2  11993  xleadd1  13175  xltadd2  13177  xlemul1  13210  xltmul2  13213  elfzo  13582  modcyc2  13829  faclbnd5  14223  relexprel  14964  subcn2  15520  mulcn2  15521  ndvdsp1  16340  gcddiv  16480  lcmneg  16532  lubel  18438  mndpfsupp  18659  gsumccatsn  18735  mulgaddcom  18995  oddvdsi  19445  odcong  19446  odeq  19447  efgsp1  19634  lspsnss  20911  rnglidlrng  21172  lindsmm2  21754  mulmarep1el  22475  mdetunilem4  22518  iuncld  22948  neips  23016  opnneip  23022  comppfsc  23435  hmeof1o2  23666  ordthmeo  23705  ufinffr  23832  elfm3  23853  utop3cls  24155  blcntrps  24316  blcntr  24317  neibl  24405  blnei  24406  metss  24412  stdbdmetval  24418  prdsms  24435  blval2  24466  lmmbr  25174  lmmbr2  25175  iscau2  25193  bcthlem1  25240  bcthlem3  25242  bcthlem4  25243  dvn2bss  25848  dvfsumrlim  25954  dvfsumrlim2  25955  cxpexpz  26592  cxpsub  26607  cxpcom  26664  relogbzexp  26702  sltsub1  28003  1ewlk  30077  1pthon2ve  30116  upgr4cycl4dv4e  30147  konigsbergssiedgwpr  30211  dlwwlknondlwlknonf1o  30327  hvaddsub12  31000  hvaddsubass  31003  hvsubdistr1  31011  hvsubcan  31036  hhssnv  31226  spanunsni  31541  homco1  31763  homulass  31764  hoadddir  31766  hosubdi  31770  hoaddsubass  31777  hosubsub4  31780  lnopmi  31962  adjlnop  32048  mdsymlem5  32369  disjif  32540  disjif2  32543  ind0  32814  sigaclfu  34088  signstfvc  34544  bnj544  34863  bnj561  34872  bnj562  34873  bnj594  34881  swrdrevpfx  35092  satfvsuc  35336  satfvsucsuc  35340  clsint2  36305  weiunso  36442  weiunwe  36445  ftc1anclem6  37680  isbnd2  37765  blbnd  37769  isdrngo2  37940  atnem0  39299  hlrelat5N  39383  ltrnel  40121  ltrnat  40122  ltrncnvat  40123  nnproddivdvdsd  41976  dvdsexpnn  42309  jm2.22  42971  jm2.23  42972  dvconstbi  44310  eelT11  44683  eelT12  44685  eelTT1  44686  eelT01  44687  eel0T1  44688  liminfvalxr  45768  grlimprclnbgr  47984  rmfsupp  48361  scmfsupp  48363  dignn0flhalflem2  48605  rrx2vlinest  48730  rrx2linesl  48732