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 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  1180  3adant3r  1181  syl3an3b  1405  syl3an3br  1408  disji  5151  ovmpox  7603  ovmpoga  7604  wrecseq123  8355  wfrlem14OLD  8378  dif1en  9226  dif1enOLD  9228  domtrfil  9258  ssdomfi2  9263  domnsymfi  9266  sdomdomtrfi  9267  domsdomtrfi  9268  phplem2  9271  php  9273  php3  9275  findcard3  9346  unbnn2  9361  axdc3lem4  10522  axdclem2  10589  gruiin  10879  gruen  10881  divass  11967  ltmul2  12145  xleadd1  13317  xltadd2  13319  xlemul1  13352  xltmul2  13355  elfzo  13718  modcyc2  13958  faclbnd5  14347  relexprel  15088  subcn2  15641  mulcn2  15642  ndvdsp1  16459  gcddiv  16598  lcmneg  16650  lubel  18584  gsumccatsn  18878  mulgaddcom  19138  oddvdsi  19590  odcong  19591  odeq  19592  efgsp1  19779  lspsnss  21011  rnglidlrng  21280  lindsmm2  21872  mulmarep1el  22599  mdetunilem4  22642  iuncld  23074  neips  23142  opnneip  23148  comppfsc  23561  hmeof1o2  23792  ordthmeo  23831  ufinffr  23958  elfm3  23979  utop3cls  24281  blcntrps  24443  blcntr  24444  neibl  24535  blnei  24536  metss  24542  stdbdmetval  24548  prdsms  24565  blval2  24596  lmmbr  25311  lmmbr2  25312  iscau2  25330  bcthlem1  25377  bcthlem3  25379  bcthlem4  25380  dvn2bss  25986  dvfsumrlim  26092  dvfsumrlim2  26093  cxpexpz  26727  cxpsub  26742  cxpcom  26799  relogbzexp  26837  sltsub1  28124  1ewlk  30147  1pthon2ve  30186  upgr4cycl4dv4e  30217  konigsbergssiedgwpr  30281  dlwwlknondlwlknonf1o  30397  hvaddsub12  31070  hvaddsubass  31073  hvsubdistr1  31081  hvsubcan  31106  hhssnv  31296  spanunsni  31611  homco1  31833  homulass  31834  hoadddir  31836  hosubdi  31840  hoaddsubass  31847  hosubsub4  31850  lnopmi  32032  adjlnop  32118  mdsymlem5  32439  disjif  32600  disjif2  32603  ind0  33982  sigaclfu  34083  signstfvc  34551  bnj544  34870  bnj561  34879  bnj562  34880  bnj594  34888  swrdrevpfx  35084  satfvsuc  35329  satfvsucsuc  35333  clsint2  36295  weiunso  36432  weiunwe  36435  ftc1anclem6  37658  isbnd2  37743  blbnd  37747  isdrngo2  37918  atnem0  39274  hlrelat5N  39358  ltrnel  40096  ltrnat  40097  ltrncnvat  40098  nnproddivdvdsd  41957  dvdsexpnn  42320  jm2.22  42952  jm2.23  42953  dvconstbi  44303  eelT11  44678  eelT12  44680  eelTT1  44681  eelT01  44682  eel0T1  44683  liminfvalxr  45704  rmfsupp  48099  mndpfsupp  48101  scmfsupp  48103  dignn0flhalflem2  48350  rrx2vlinest  48475  rrx2linesl  48477