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  5070  ovmpox  7520  ovmpoga  7521  wrecseq123  8263  dif1en  9096  domtrfil  9126  ssdomfi2  9131  domnsymfi  9134  sdomdomtrfi  9135  domsdomtrfi  9136  phplem2  9139  php  9141  php3  9143  findcard3  9193  unbnn2  9207  axdc3lem4  10375  axdclem2  10442  gruiin  10733  gruen  10735  divass  11827  ltmul2  12006  ind0  12169  xleadd1  13207  xltadd2  13209  xlemul1  13242  xltmul2  13245  elfzo  13615  modcyc2  13866  faclbnd5  14260  relexprel  15001  subcn2  15557  mulcn2  15558  ndvdsp1  16380  gcddiv  16520  lcmneg  16572  lubel  18480  mndpfsupp  18735  gsumccatsn  18811  mulgaddcom  19074  oddvdsi  19523  odcong  19524  odeq  19525  efgsp1  19712  lspsnss  20985  rnglidlrng  21245  lindsmm2  21809  mulmarep1el  22537  mdetunilem4  22580  iuncld  23010  neips  23078  opnneip  23084  comppfsc  23497  hmeof1o2  23728  ordthmeo  23767  ufinffr  23894  elfm3  23915  utop3cls  24216  blcntrps  24377  blcntr  24378  neibl  24466  blnei  24467  metss  24473  stdbdmetval  24479  prdsms  24496  blval2  24527  lmmbr  25225  lmmbr2  25226  iscau2  25244  bcthlem1  25291  bcthlem3  25293  bcthlem4  25294  dvn2bss  25897  dvfsumrlim  25998  dvfsumrlim2  25999  cxpexpz  26631  cxpsub  26646  cxpcom  26703  relogbzexp  26740  ltsubs1  28068  1ewlk  30185  1pthon2ve  30224  upgr4cycl4dv4e  30255  konigsbergssiedgwpr  30319  dlwwlknondlwlknonf1o  30435  hvaddsub12  31109  hvaddsubass  31112  hvsubdistr1  31120  hvsubcan  31145  hhssnv  31335  spanunsni  31650  homco1  31872  homulass  31873  hoadddir  31875  hosubdi  31879  hoaddsubass  31886  hosubsub4  31889  lnopmi  32071  adjlnop  32157  mdsymlem5  32478  disjif  32648  disjif2  32651  sigaclfu  34263  signstfvc  34718  bnj544  35036  bnj561  35045  bnj562  35046  bnj594  35054  fineqvnttrclselem3  35267  swrdrevpfx  35299  satfvsuc  35543  satfvsucsuc  35547  clsint2  36511  weiunso  36648  weiunwe  36651  ftc1anclem6  38019  isbnd2  38104  blbnd  38108  isdrngo2  38279  atnem0  39764  hlrelat5N  39847  ltrnel  40585  ltrnat  40586  ltrncnvat  40587  nnproddivdvdsd  42439  dvdsexpnn  42765  jm2.22  43423  jm2.23  43424  dvconstbi  44761  eelT11  45133  eelT12  45135  eelTT1  45136  eelT01  45137  eel0T1  45138  liminfvalxr  46211  grlimprclnbgr  48472  rmfsupp  48849  scmfsupp  48851  dignn0flhalflem2  49092  rrx2vlinest  49217  rrx2linesl  49219