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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3adant3l  1181  3adant3r  1182  syl3an3b  1406  syl3an3br  1409  disji  5132  ovmpox  7561  ovmpoga  7562  wrecseq123  8299  wfrlem14OLD  8322  dif1en  9160  dif1enOLD  9162  domtrfil  9195  ssdomfi2  9200  domnsymfi  9203  sdomdomtrfi  9204  domsdomtrfi  9205  phplem2  9208  php  9210  php3  9212  findcard3  9285  unbnn2  9300  axdc3lem4  10448  axdclem2  10515  gruiin  10805  gruen  10807  divass  11890  ltmul2  12065  xleadd1  13234  xltadd2  13236  xlemul1  13269  xltmul2  13272  elfzo  13634  modcyc2  13872  faclbnd5  14258  relexprel  14986  subcn2  15539  mulcn2  15540  ndvdsp1  16354  gcddiv  16493  lcmneg  16540  lubel  18467  gsumccatsn  18724  mulgaddcom  18978  oddvdsi  19416  odcong  19417  odeq  19418  efgsp1  19605  lspsnss  20601  lindsmm2  21384  mulmarep1el  22074  mdetunilem4  22117  iuncld  22549  neips  22617  opnneip  22623  comppfsc  23036  hmeof1o2  23267  ordthmeo  23306  ufinffr  23433  elfm3  23454  utop3cls  23756  blcntrps  23918  blcntr  23919  neibl  24010  blnei  24011  metss  24017  stdbdmetval  24023  prdsms  24040  blval2  24071  lmmbr  24775  lmmbr2  24776  iscau2  24794  bcthlem1  24841  bcthlem3  24843  bcthlem4  24844  dvn2bss  25447  dvfsumrlim  25548  dvfsumrlim2  25549  cxpexpz  26175  cxpsub  26190  cxpcom  26247  relogbzexp  26281  sltsub1  27543  1ewlk  29368  1pthon2ve  29407  upgr4cycl4dv4e  29438  konigsbergssiedgwpr  29502  dlwwlknondlwlknonf1o  29618  hvaddsub12  30291  hvaddsubass  30294  hvsubdistr1  30302  hvsubcan  30327  hhssnv  30517  spanunsni  30832  homco1  31054  homulass  31055  hoadddir  31057  hosubdi  31061  hoaddsubass  31068  hosubsub4  31071  lnopmi  31253  adjlnop  31339  mdsymlem5  31660  disjif  31809  disjif2  31812  ind0  33016  sigaclfu  33117  signstfvc  33585  bnj544  33905  bnj561  33914  bnj562  33915  bnj594  33923  swrdrevpfx  34107  satfvsuc  34352  satfvsucsuc  34356  clsint2  35214  ftc1anclem6  36566  isbnd2  36651  blbnd  36655  isdrngo2  36826  atnem0  38188  hlrelat5N  38272  ltrnel  39010  ltrnat  39011  ltrncnvat  39012  nnproddivdvdsd  40866  dvdsexpnn  41231  jm2.22  41734  jm2.23  41735  dvconstbi  43093  eelT11  43468  eelT12  43470  eelTT1  43471  eelT01  43472  eel0T1  43473  liminfvalxr  44499  rnglidlrng  46758  rmfsupp  47050  mndpfsupp  47052  scmfsupp  47054  dignn0flhalflem2  47302  rrx2vlinest  47427  rrx2linesl  47429