Theorem syl3an3 1166

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant3l  1182  3adant3r  1183  syl3an3b  1408  syl3an3br  1411  disji  5071  ovmpox  7513  ovmpoga  7514  wrecseq123  8256  dif1en  9089  domtrfil  9119  ssdomfi2  9124  domnsymfi  9127  sdomdomtrfi  9128  domsdomtrfi  9129  phplem2  9132  php  9134  php3  9136  findcard3  9186  unbnn2  9200  axdc3lem4  10366  axdclem2  10433  gruiin  10724  gruen  10726  divass  11818  ltmul2  11997  ind0  12160  xleadd1  13198  xltadd2  13200  xlemul1  13233  xltmul2  13236  elfzo  13606  modcyc2  13857  faclbnd5  14251  relexprel  14992  subcn2  15548  mulcn2  15549  ndvdsp1  16371  gcddiv  16511  lcmneg  16563  lubel  18471  mndpfsupp  18726  gsumccatsn  18802  mulgaddcom  19065  oddvdsi  19514  odcong  19515  odeq  19516  efgsp1  19703  lspsnss  20976  rnglidlrng  21237  lindsmm2  21819  mulmarep1el  22547  mdetunilem4  22590  iuncld  23020  neips  23088  opnneip  23094  comppfsc  23507  hmeof1o2  23738  ordthmeo  23777  ufinffr  23904  elfm3  23925  utop3cls  24226  blcntrps  24387  blcntr  24388  neibl  24476  blnei  24477  metss  24483  stdbdmetval  24489  prdsms  24506  blval2  24537  lmmbr  25235  lmmbr2  25236  iscau2  25254  bcthlem1  25301  bcthlem3  25303  bcthlem4  25304  dvn2bss  25907  dvfsumrlim  26008  dvfsumrlim2  26009  cxpexpz  26644  cxpsub  26659  cxpcom  26716  relogbzexp  26753  ltsubs1  28082  1ewlk  30200  1pthon2ve  30239  upgr4cycl4dv4e  30270  konigsbergssiedgwpr  30334  dlwwlknondlwlknonf1o  30450  hvaddsub12  31124  hvaddsubass  31127  hvsubdistr1  31135  hvsubcan  31160  hhssnv  31350  spanunsni  31665  homco1  31887  homulass  31888  hoadddir  31890  hosubdi  31894  hoaddsubass  31901  hosubsub4  31904  lnopmi  32086  adjlnop  32172  mdsymlem5  32493  disjif  32663  disjif2  32666  sigaclfu  34279  signstfvc  34734  bnj544  35052  bnj561  35061  bnj562  35062  bnj594  35070  fineqvnttrclselem3  35283  swrdrevpfx  35315  satfvsuc  35559  satfvsucsuc  35563  clsint2  36527  weiunso  36664  weiunwe  36667  ftc1anclem6  38033  isbnd2  38118  blbnd  38122  isdrngo2  38293  atnem0  39778  hlrelat5N  39861  ltrnel  40599  ltrnat  40600  ltrncnvat  40601  nnproddivdvdsd  42453  dvdsexpnn  42779  jm2.22  43441  jm2.23  43442  dvconstbi  44779  eelT11  45151  eelT12  45153  eelTT1  45154  eelT01  45155  eel0T1  45156  liminfvalxr  46229  grlimprclnbgr  48484  rmfsupp  48861  scmfsupp  48863  dignn0flhalflem2  49104  rrx2vlinest  49229  rrx2linesl  49231