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  5071  ovmpox  7494  ovmpoga  7495  wrecseq123  8238  dif1en  9066  domtrfil  9096  ssdomfi2  9101  domnsymfi  9104  sdomdomtrfi  9105  domsdomtrfi  9106  phplem2  9109  php  9111  php3  9113  findcard3  9162  unbnn2  9176  axdc3lem4  10339  axdclem2  10406  gruiin  10696  gruen  10698  divass  11789  ltmul2  11967  xleadd1  13149  xltadd2  13151  xlemul1  13184  xltmul2  13187  elfzo  13556  modcyc2  13806  faclbnd5  14200  relexprel  14941  subcn2  15497  mulcn2  15498  ndvdsp1  16317  gcddiv  16457  lcmneg  16509  lubel  18415  mndpfsupp  18670  gsumccatsn  18746  mulgaddcom  19006  oddvdsi  19455  odcong  19456  odeq  19457  efgsp1  19644  lspsnss  20918  rnglidlrng  21179  lindsmm2  21761  mulmarep1el  22482  mdetunilem4  22525  iuncld  22955  neips  23023  opnneip  23029  comppfsc  23442  hmeof1o2  23673  ordthmeo  23712  ufinffr  23839  elfm3  23860  utop3cls  24161  blcntrps  24322  blcntr  24323  neibl  24411  blnei  24412  metss  24418  stdbdmetval  24424  prdsms  24441  blval2  24472  lmmbr  25180  lmmbr2  25181  iscau2  25199  bcthlem1  25246  bcthlem3  25248  bcthlem4  25249  dvn2bss  25854  dvfsumrlim  25960  dvfsumrlim2  25961  cxpexpz  26598  cxpsub  26613  cxpcom  26670  relogbzexp  26708  sltsub1  28011  1ewlk  30087  1pthon2ve  30126  upgr4cycl4dv4e  30157  konigsbergssiedgwpr  30221  dlwwlknondlwlknonf1o  30337  hvaddsub12  31010  hvaddsubass  31013  hvsubdistr1  31021  hvsubcan  31046  hhssnv  31236  spanunsni  31551  homco1  31773  homulass  31774  hoadddir  31776  hosubdi  31780  hoaddsubass  31787  hosubsub4  31790  lnopmi  31972  adjlnop  32058  mdsymlem5  32379  disjif  32550  disjif2  32553  ind0  32831  sigaclfu  34124  signstfvc  34579  bnj544  34898  bnj561  34907  bnj562  34908  bnj594  34916  fineqvnttrclselem3  35135  swrdrevpfx  35153  satfvsuc  35397  satfvsucsuc  35401  clsint2  36363  weiunso  36500  weiunwe  36503  ftc1anclem6  37738  isbnd2  37823  blbnd  37827  isdrngo2  37998  atnem0  39357  hlrelat5N  39440  ltrnel  40178  ltrnat  40179  ltrncnvat  40180  nnproddivdvdsd  42033  dvdsexpnn  42366  jm2.22  43028  jm2.23  43029  dvconstbi  44367  eelT11  44739  eelT12  44741  eelTT1  44742  eelT01  44743  eel0T1  44744  liminfvalxr  45821  grlimprclnbgr  48027  rmfsupp  48404  scmfsupp  48406  dignn0flhalflem2  48648  rrx2vlinest  48773  rrx2linesl  48775