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  5074  ovmpox  7499  ovmpoga  7500  wrecseq123  8243  dif1en  9071  domtrfil  9101  ssdomfi2  9106  domnsymfi  9109  sdomdomtrfi  9110  domsdomtrfi  9111  phplem2  9114  php  9116  php3  9118  findcard3  9167  unbnn2  9181  axdc3lem4  10344  axdclem2  10411  gruiin  10701  gruen  10703  divass  11794  ltmul2  11972  xleadd1  13154  xltadd2  13156  xlemul1  13189  xltmul2  13192  elfzo  13561  modcyc2  13811  faclbnd5  14205  relexprel  14946  subcn2  15502  mulcn2  15503  ndvdsp1  16322  gcddiv  16462  lcmneg  16514  lubel  18420  mndpfsupp  18675  gsumccatsn  18751  mulgaddcom  19011  oddvdsi  19460  odcong  19461  odeq  19462  efgsp1  19649  lspsnss  20923  rnglidlrng  21184  lindsmm2  21766  mulmarep1el  22487  mdetunilem4  22530  iuncld  22960  neips  23028  opnneip  23034  comppfsc  23447  hmeof1o2  23678  ordthmeo  23717  ufinffr  23844  elfm3  23865  utop3cls  24166  blcntrps  24327  blcntr  24328  neibl  24416  blnei  24417  metss  24423  stdbdmetval  24429  prdsms  24446  blval2  24477  lmmbr  25185  lmmbr2  25186  iscau2  25204  bcthlem1  25251  bcthlem3  25253  bcthlem4  25254  dvn2bss  25859  dvfsumrlim  25965  dvfsumrlim2  25966  cxpexpz  26603  cxpsub  26618  cxpcom  26675  relogbzexp  26713  sltsub1  28016  1ewlk  30095  1pthon2ve  30134  upgr4cycl4dv4e  30165  konigsbergssiedgwpr  30229  dlwwlknondlwlknonf1o  30345  hvaddsub12  31018  hvaddsubass  31021  hvsubdistr1  31029  hvsubcan  31054  hhssnv  31244  spanunsni  31559  homco1  31781  homulass  31782  hoadddir  31784  hosubdi  31788  hoaddsubass  31795  hosubsub4  31798  lnopmi  31980  adjlnop  32066  mdsymlem5  32387  disjif  32558  disjif2  32561  ind0  32839  sigaclfu  34132  signstfvc  34587  bnj544  34906  bnj561  34915  bnj562  34916  bnj594  34924  fineqvnttrclselem3  35143  swrdrevpfx  35161  satfvsuc  35405  satfvsucsuc  35409  clsint2  36373  weiunso  36510  weiunwe  36513  ftc1anclem6  37737  isbnd2  37822  blbnd  37826  isdrngo2  37997  atnem0  39416  hlrelat5N  39499  ltrnel  40237  ltrnat  40238  ltrncnvat  40239  nnproddivdvdsd  42092  dvdsexpnn  42425  jm2.22  43087  jm2.23  43088  dvconstbi  44426  eelT11  44798  eelT12  44800  eelTT1  44801  eelT01  44802  eel0T1  44803  liminfvalxr  45880  grlimprclnbgr  48095  rmfsupp  48472  scmfsupp  48474  dignn0flhalflem2  48716  rrx2vlinest  48841  rrx2linesl  48843