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  5080  ovmpox  7508  ovmpoga  7509  wrecseq123  8252  dif1en  9082  domtrfil  9112  ssdomfi2  9117  domnsymfi  9120  sdomdomtrfi  9121  domsdomtrfi  9122  phplem2  9125  php  9127  php3  9129  findcard3  9178  unbnn2  9192  axdc3lem4  10355  axdclem2  10422  gruiin  10712  gruen  10714  divass  11805  ltmul2  11983  xleadd1  13161  xltadd2  13163  xlemul1  13196  xltmul2  13199  elfzo  13568  modcyc2  13818  faclbnd5  14212  relexprel  14953  subcn2  15509  mulcn2  15510  ndvdsp1  16329  gcddiv  16469  lcmneg  16521  lubel  18428  mndpfsupp  18683  gsumccatsn  18759  mulgaddcom  19019  oddvdsi  19468  odcong  19469  odeq  19470  efgsp1  19657  lspsnss  20932  rnglidlrng  21193  lindsmm2  21775  mulmarep1el  22507  mdetunilem4  22550  iuncld  22980  neips  23048  opnneip  23054  comppfsc  23467  hmeof1o2  23698  ordthmeo  23737  ufinffr  23864  elfm3  23885  utop3cls  24186  blcntrps  24347  blcntr  24348  neibl  24436  blnei  24437  metss  24443  stdbdmetval  24449  prdsms  24466  blval2  24497  lmmbr  25205  lmmbr2  25206  iscau2  25224  bcthlem1  25271  bcthlem3  25273  bcthlem4  25274  dvn2bss  25879  dvfsumrlim  25985  dvfsumrlim2  25986  cxpexpz  26623  cxpsub  26638  cxpcom  26695  relogbzexp  26733  sltsub1  28036  1ewlk  30116  1pthon2ve  30155  upgr4cycl4dv4e  30186  konigsbergssiedgwpr  30250  dlwwlknondlwlknonf1o  30366  hvaddsub12  31039  hvaddsubass  31042  hvsubdistr1  31050  hvsubcan  31075  hhssnv  31265  spanunsni  31580  homco1  31802  homulass  31803  hoadddir  31805  hosubdi  31809  hoaddsubass  31816  hosubsub4  31819  lnopmi  32001  adjlnop  32087  mdsymlem5  32408  disjif  32579  disjif2  32582  ind0  32865  sigaclfu  34204  signstfvc  34659  bnj544  34978  bnj561  34987  bnj562  34988  bnj594  34996  fineqvnttrclselem3  35215  swrdrevpfx  35233  satfvsuc  35477  satfvsucsuc  35481  clsint2  36445  weiunso  36582  weiunwe  36585  ftc1anclem6  37811  isbnd2  37896  blbnd  37900  isdrngo2  38071  atnem0  39490  hlrelat5N  39573  ltrnel  40311  ltrnat  40312  ltrncnvat  40313  nnproddivdvdsd  42166  dvdsexpnn  42503  jm2.22  43152  jm2.23  43153  dvconstbi  44491  eelT11  44863  eelT12  44865  eelTT1  44866  eelT01  44867  eel0T1  44868  liminfvalxr  45943  grlimprclnbgr  48158  rmfsupp  48535  scmfsupp  48537  dignn0flhalflem2  48778  rrx2vlinest  48903  rrx2linesl  48905