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  27546  1ewlk  29399  1pthon2ve  29438  upgr4cycl4dv4e  29469  konigsbergssiedgwpr  29533  dlwwlknondlwlknonf1o  29649  hvaddsub12  30322  hvaddsubass  30325  hvsubdistr1  30333  hvsubcan  30358  hhssnv  30548  spanunsni  30863  homco1  31085  homulass  31086  hoadddir  31088  hosubdi  31092  hoaddsubass  31099  hosubsub4  31102  lnopmi  31284  adjlnop  31370  mdsymlem5  31691  disjif  31840  disjif2  31843  ind0  33047  sigaclfu  33148  signstfvc  33616  bnj544  33936  bnj561  33945  bnj562  33946  bnj594  33954  swrdrevpfx  34138  satfvsuc  34383  satfvsucsuc  34387  clsint2  35262  ftc1anclem6  36614  isbnd2  36699  blbnd  36703  isdrngo2  36874  atnem0  38236  hlrelat5N  38320  ltrnel  39058  ltrnat  39059  ltrncnvat  39060  nnproddivdvdsd  40914  dvdsexpnn  41279  jm2.22  41782  jm2.23  41783  dvconstbi  43141  eelT11  43516  eelT12  43518  eelTT1  43519  eelT01  43520  eel0T1  43521  liminfvalxr  44547  rnglidlrng  46806  rmfsupp  47098  mndpfsupp  47100  scmfsupp  47102  dignn0flhalflem2  47350  rrx2vlinest  47475  rrx2linesl  47477