Theorem syl3an3 1162

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3adant3l  1177  3adant3r  1178  syl3an3b  1402  syl3an3br  1405  disji  5136  ovmpox  7579  ovmpoga  7580  wrecseq123  8329  wfrlem14OLD  8352  dif1en  9198  dif1enOLD  9200  domtrfil  9229  ssdomfi2  9234  domnsymfi  9237  sdomdomtrfi  9238  domsdomtrfi  9239  phplem2  9242  php  9244  php3  9246  findcard3  9319  unbnn2  9334  axdc3lem4  10496  axdclem2  10563  gruiin  10853  gruen  10855  divass  11941  ltmul2  12116  xleadd1  13288  xltadd2  13290  xlemul1  13323  xltmul2  13326  elfzo  13688  modcyc2  13927  faclbnd5  14315  relexprel  15044  subcn2  15597  mulcn2  15598  ndvdsp1  16413  gcddiv  16552  lcmneg  16604  lubel  18539  gsumccatsn  18833  mulgaddcom  19092  oddvdsi  19546  odcong  19547  odeq  19548  efgsp1  19735  lspsnss  20967  rnglidlrng  21236  lindsmm2  21827  mulmarep1el  22565  mdetunilem4  22608  iuncld  23040  neips  23108  opnneip  23114  comppfsc  23527  hmeof1o2  23758  ordthmeo  23797  ufinffr  23924  elfm3  23945  utop3cls  24247  blcntrps  24409  blcntr  24410  neibl  24501  blnei  24502  metss  24508  stdbdmetval  24514  prdsms  24531  blval2  24562  lmmbr  25277  lmmbr2  25278  iscau2  25296  bcthlem1  25343  bcthlem3  25345  bcthlem4  25346  dvn2bss  25951  dvfsumrlim  26057  dvfsumrlim2  26058  cxpexpz  26694  cxpsub  26709  cxpcom  26766  relogbzexp  26804  sltsub1  28083  1ewlk  30048  1pthon2ve  30087  upgr4cycl4dv4e  30118  konigsbergssiedgwpr  30182  dlwwlknondlwlknonf1o  30298  hvaddsub12  30971  hvaddsubass  30974  hvsubdistr1  30982  hvsubcan  31007  hhssnv  31197  spanunsni  31512  homco1  31734  homulass  31735  hoadddir  31737  hosubdi  31741  hoaddsubass  31748  hosubsub4  31751  lnopmi  31933  adjlnop  32019  mdsymlem5  32340  disjif  32498  disjif2  32501  ind0  33851  sigaclfu  33952  signstfvc  34420  bnj544  34739  bnj561  34748  bnj562  34749  bnj594  34757  swrdrevpfx  34944  satfvsuc  35189  satfvsucsuc  35193  clsint2  36041  ftc1anclem6  37399  isbnd2  37484  blbnd  37488  isdrngo2  37659  atnem0  39016  hlrelat5N  39100  ltrnel  39838  ltrnat  39839  ltrncnvat  39840  nnproddivdvdsd  41699  dvdsexpnn  42128  jm2.22  42653  jm2.23  42654  dvconstbi  44008  eelT11  44383  eelT12  44385  eelTT1  44386  eelT01  44387  eel0T1  44388  liminfvalxr  45404  rmfsupp  47753  mndpfsupp  47755  scmfsupp  47757  dignn0flhalflem2  48004  rrx2vlinest  48129  rrx2linesl  48131