Theorem syl3an3 1181

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant3l  1197  3adant3r  1198  syl3an3b  1430  syl3an3br  1433  disji  5095  ovmpox  7561  ovmpoga  7562  wrecseq123  8306  dif1en  9142  domtrfil  9172  ssdomfi2  9177  domnsymfi  9180  sdomdomtrfi  9181  domsdomtrfi  9182  phplem2  9185  php  9187  php3  9189  findcard3  9239  unbnn2  9253  axdc3lem4  10433  axdclem2  10500  gruiin  10791  gruen  10793  divass  11886  ltmul2  12062  ind0  12224  xleadd1  13277  xltadd2  13279  xlemul1  13312  xltmul2  13315  elfzo  13685  modcyc2  13936  faclbnd5  14330  relexprel  15072  subcn2  15642  mulcn2  15643  ndvdsp1  16465  gcddiv  16605  lcmneg  16657  lubel  18566  mndpfsupp  18821  gsumccatsn  18898  mulgaddcom  19160  oddvdsi  19614  odcong  19615  odeq  19616  efgsp1  19803  lspsnss  21085  rnglidlrng  21351  lindsmm2  21944  mulmarep1el  22694  mdetunilem4  22737  iuncld  23167  neips  23235  opnneip  23241  comppfsc  23654  hmeof1o2  23885  ordthmeo  23924  ufinffr  24051  elfm3  24072  utop3cls  24373  blcntrps  24534  blcntr  24535  neibl  24623  blnei  24624  metss  24630  stdbdmetval  24636  prdsms  24653  blval2  24684  lmmbr  25382  lmmbr2  25383  iscau2  25401  bcthlem1  25448  bcthlem3  25450  bcthlem4  25451  dvn2bss  26054  dvfsumrlim  26155  dvfsumrlim2  26156  cxpexpz  26794  cxpsub  26809  cxpcom  26866  relogbzexp  26903  ltsubs1  28231  1ewlk  30403  1pthon2ve  30442  upgr4cycl4dv4e  30473  konigsbergssiedgwpr  30537  dlwwlknondlwlknonf1o  30653  hvaddsub12  31327  hvaddsubass  31330  hvsubdistr1  31338  hvsubcan  31363  hhssnv  31553  spanunsni  31868  homco1  32090  homulass  32091  hoadddir  32093  hosubdi  32097  hoaddsubass  32104  hosubsub4  32107  lnopmi  32289  adjlnop  32375  mdsymlem5  32696  disjif  32860  disjif2  32863  sigaclfu  34450  signstfvc  34902  bnj544  35223  bnj561  35232  bnj562  35233  bnj594  35241  fineqvnttrclselem3  35455  swrdrevpfx  35503  satfvsuc  35748  satfvsucsuc  35752  clsint2  36725  weiunso  36862  weiunwe  36865  ftc1anclem6  38232  isbnd2  38317  blbnd  38321  isdrngo2  38492  atnem0  39977  hlrelat5N  40060  ltrnel  40798  ltrnat  40799  ltrncnvat  40800  nnproddivdvdsd  42652  dvdsexpnn  42977  jm2.22  43607  jm2.23  43608  dvconstbi  44929  eelT11  45300  eelT12  45302  eelTT1  45303  eelT01  45304  eel0T1  45305  liminfvalxr  46382  grlimprclnbgr  48643  rmfsupp  49031  scmfsupp  49033  dignn0flhalflem2  49274  rrx2vlinest  49399  rrx2linesl  49401