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  5087  ovmpox  7522  ovmpoga  7523  wrecseq123  8269  dif1en  9101  dif1enOLD  9103  domtrfil  9133  ssdomfi2  9138  domnsymfi  9141  sdomdomtrfi  9142  domsdomtrfi  9143  phplem2  9146  php  9148  php3  9150  findcard3  9205  unbnn2  9220  axdc3lem4  10382  axdclem2  10449  gruiin  10739  gruen  10741  divass  11831  ltmul2  12009  xleadd1  13191  xltadd2  13193  xlemul1  13226  xltmul2  13229  elfzo  13598  modcyc2  13845  faclbnd5  14239  relexprel  14981  subcn2  15537  mulcn2  15538  ndvdsp1  16357  gcddiv  16497  lcmneg  16549  lubel  18449  mndpfsupp  18670  gsumccatsn  18746  mulgaddcom  19006  oddvdsi  19454  odcong  19455  odeq  19456  efgsp1  19643  lspsnss  20872  rnglidlrng  21133  lindsmm2  21714  mulmarep1el  22435  mdetunilem4  22478  iuncld  22908  neips  22976  opnneip  22982  comppfsc  23395  hmeof1o2  23626  ordthmeo  23665  ufinffr  23792  elfm3  23813  utop3cls  24115  blcntrps  24276  blcntr  24277  neibl  24365  blnei  24366  metss  24372  stdbdmetval  24378  prdsms  24395  blval2  24426  lmmbr  25134  lmmbr2  25135  iscau2  25153  bcthlem1  25200  bcthlem3  25202  bcthlem4  25203  dvn2bss  25808  dvfsumrlim  25914  dvfsumrlim2  25915  cxpexpz  26552  cxpsub  26567  cxpcom  26624  relogbzexp  26662  sltsub1  27956  1ewlk  30017  1pthon2ve  30056  upgr4cycl4dv4e  30087  konigsbergssiedgwpr  30151  dlwwlknondlwlknonf1o  30267  hvaddsub12  30940  hvaddsubass  30943  hvsubdistr1  30951  hvsubcan  30976  hhssnv  31166  spanunsni  31481  homco1  31703  homulass  31704  hoadddir  31706  hosubdi  31710  hoaddsubass  31717  hosubsub4  31720  lnopmi  31902  adjlnop  31988  mdsymlem5  32309  disjif  32480  disjif2  32483  ind0  32754  sigaclfu  34082  signstfvc  34538  bnj544  34857  bnj561  34866  bnj562  34867  bnj594  34875  swrdrevpfx  35077  satfvsuc  35321  satfvsucsuc  35325  clsint2  36290  weiunso  36427  weiunwe  36430  ftc1anclem6  37665  isbnd2  37750  blbnd  37754  isdrngo2  37925  atnem0  39284  hlrelat5N  39368  ltrnel  40106  ltrnat  40107  ltrncnvat  40108  nnproddivdvdsd  41961  dvdsexpnn  42294  jm2.22  42957  jm2.23  42958  dvconstbi  44296  eelT11  44669  eelT12  44671  eelTT1  44672  eelT01  44673  eel0T1  44674  liminfvalxr  45754  rmfsupp  48334  scmfsupp  48336  dignn0flhalflem2  48578  rrx2vlinest  48703  rrx2linesl  48705