Theorem syl3an3 1183

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3l  1199  3adant3r  1200  syl3an3b  1433  syl3an3br  1436  disji  5093  ovmpox  7605  ovmpoga  7606  wrecseq123  8369  tz7.48lem  8488  dif1en  9215  domtrfil  9245  ssdomfi2  9250  domnsymfi  9253  sdomdomtrfi  9254  domsdomtrfi  9255  phplem2  9258  php  9260  php3  9262  findcard3  9312  unbnn2  9327  axdc3lem4  10570  axdclem2  10637  gruiin  10934  gruen  10936  divass  12032  ltmul2  12208  ind0  12370  xleadd1  13425  xltadd2  13427  xlemul1  13460  xltmul2  13463  elfzo  13835  modcyc2  14087  faclbnd5  14483  swrdrevpfx  14960  relexprel  15235  subcn2  15806  mulcn2  15807  ndvdsp1  16625  gcddiv  16768  dvdsexpnn  16784  lcmneg  16822  lubel  18738  mndpfsupp  19011  gsumccatsn  19089  mulgaddcom  19358  oddvdsi  19813  odcong  19814  odeq  19815  efgsp1  20002  lspsnss  21316  rnglidlrng  21586  lindsmm2  22190  mulmarep1el  22942  mdetunilem4  22985  iuncld  23418  neips  23486  opnneip  23492  comppfsc  23906  hmeof1o2  24137  ordthmeo  24176  ufinffr  24303  elfm3  24324  utop3cls  24625  blcntrps  24786  blcntr  24787  neibl  24875  blnei  24876  metss  24882  stdbdmetval  24888  prdsms  24905  blval2  24936  lmmbr  25634  lmmbr2  25635  iscau2  25653  bcthlem1  25700  bcthlem3  25702  bcthlem4  25703  dvn2bss  26305  dvfsumrlim  26406  dvfsumrlim2  26407  cxpexpz  27052  cxpsub  27067  cxpcom  27124  relogbzexp  27161  ltsubs1  28519  1ewlk  30763  1pthon2ve  30812  upgr4cycl4dv4e  30843  konigsbergssiedgwpr  30907  dlwwlknondlwlknonf1o  31023  hvaddsub12  31697  hvaddsubass  31700  hvsubdistr1  31708  hvsubcan  31733  hhssnv  31923  spanunsni  32238  homco1  32460  homulass  32461  hoadddir  32463  hosubdi  32467  hoaddsubass  32474  hosubsub4  32477  lnopmi  32659  adjlnop  32745  mdsymlem5  33066  disjif  33270  disjif2  33273  sigaclfu  34862  signstfvc  35314  bnj544  35635  bnj561  35644  bnj562  35645  bnj594  35653  fineqvnttrclselem3  35932  satfvsuc  36334  satfvsucsuc  36338  clsint2  37332  weiunso  37469  weiunwe  37472  ftc1anclem6  38884  isbnd2  38983  blbnd  38987  isdrngo2  39158  atnem0  40641  hlrelat5N  40724  ltrnel  41462  ltrnat  41463  ltrncnvat  41464  nnproddivdvdsd  43316  jm2.22  44268  jm2.23  44269  dvconstbi  45579  eelT11  45949  eelT12  45951  eelTT1  45952  eelT01  45953  eel0T1  45954  liminfvalxr  47066  grlimprclnbgr  49367  rmfsupp  49816  scmfsupp  49818  dignn0flhalflem2  50059  rrx2vlinest  50184  rrx2linesl  50186