Theorem syl3an3 1171

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 1160	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant3l  1187  3adant3r  1188  syl3an3b  1413  syl3an3br  1416  disji  5064  ovmpox  7516  ovmpoga  7517  wrecseq123  8260  dif1en  9093  domtrfil  9123  ssdomfi2  9128  domnsymfi  9131  sdomdomtrfi  9132  domsdomtrfi  9133  phplem2  9136  php  9138  php3  9140  findcard3  9190  unbnn2  9204  axdc3lem4  10373  axdclem2  10440  gruiin  10731  gruen  10733  divass  11825  ltmul2  12004  ind0  12167  xleadd1  13205  xltadd2  13207  xlemul1  13240  xltmul2  13243  elfzo  13613  modcyc2  13864  faclbnd5  14258  relexprel  14999  subcn2  15555  mulcn2  15556  ndvdsp1  16378  gcddiv  16518  lcmneg  16570  lubel  18478  mndpfsupp  18733  gsumccatsn  18809  mulgaddcom  19072  oddvdsi  19521  odcong  19522  odeq  19523  efgsp1  19710  lspsnss  20987  rnglidlrng  21247  lindsmm2  21811  mulmarep1el  22562  mdetunilem4  22605  iuncld  23035  neips  23103  opnneip  23109  comppfsc  23522  hmeof1o2  23753  ordthmeo  23792  ufinffr  23919  elfm3  23940  utop3cls  24241  blcntrps  24402  blcntr  24403  neibl  24491  blnei  24492  metss  24498  stdbdmetval  24504  prdsms  24521  blval2  24552  lmmbr  25250  lmmbr2  25251  iscau2  25269  bcthlem1  25316  bcthlem3  25318  bcthlem4  25319  dvn2bss  25922  dvfsumrlim  26023  dvfsumrlim2  26024  cxpexpz  26656  cxpsub  26671  cxpcom  26728  relogbzexp  26765  ltsubs1  28093  1ewlk  30210  1pthon2ve  30249  upgr4cycl4dv4e  30280  konigsbergssiedgwpr  30344  dlwwlknondlwlknonf1o  30460  hvaddsub12  31134  hvaddsubass  31137  hvsubdistr1  31145  hvsubcan  31170  hhssnv  31360  spanunsni  31675  homco1  31897  homulass  31898  hoadddir  31900  hosubdi  31904  hoaddsubass  31911  hosubsub4  31914  lnopmi  32096  adjlnop  32182  mdsymlem5  32503  disjif  32674  disjif2  32677  sigaclfu  34310  signstfvc  34765  bnj544  35083  bnj561  35092  bnj562  35093  bnj594  35101  fineqvnttrclselem3  35311  swrdrevpfx  35352  satfvsuc  35596  satfvsucsuc  35600  clsint2  36564  weiunso  36701  weiunwe  36704  ftc1anclem6  38072  isbnd2  38157  blbnd  38161  isdrngo2  38332  atnem0  39817  hlrelat5N  39900  ltrnel  40638  ltrnat  40639  ltrncnvat  40640  nnproddivdvdsd  42492  dvdsexpnn  42817  jm2.22  43447  jm2.23  43448  dvconstbi  44785  eelT11  45157  eelT12  45159  eelTT1  45160  eelT01  45161  eel0T1  45162  liminfvalxr  46233  grlimprclnbgr  48494  rmfsupp  48871  scmfsupp  48873  dignn0flhalflem2  49114  rrx2vlinest  49239  rrx2linesl  49241