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  1432  syl3an3br  1435  disji  5088  ovmpox  7566  ovmpoga  7567  wrecseq123  8312  dif1en  9156  domtrfil  9186  ssdomfi2  9191  domnsymfi  9194  sdomdomtrfi  9195  domsdomtrfi  9196  phplem2  9199  php  9201  php3  9203  findcard3  9253  unbnn2  9267  axdc3lem4  10455  axdclem2  10522  gruiin  10819  gruen  10821  divass  11914  ltmul2  12090  ind0  12252  xleadd1  13307  xltadd2  13309  xlemul1  13342  xltmul2  13345  elfzo  13716  modcyc2  13968  faclbnd5  14362  swrdrevpfx  14838  relexprel  15112  subcn2  15682  mulcn2  15683  ndvdsp1  16501  gcddiv  16641  lcmneg  16693  lubel  18602  mndpfsupp  18874  gsumccatsn  18952  mulgaddcom  19221  oddvdsi  19675  odcong  19676  odeq  19677  efgsp1  19864  lspsnss  21174  rnglidlrng  21444  lindsmm2  22042  mulmarep1el  22794  mdetunilem4  22837  iuncld  23270  neips  23338  opnneip  23344  comppfsc  23758  hmeof1o2  23989  ordthmeo  24028  ufinffr  24155  elfm3  24176  utop3cls  24477  blcntrps  24638  blcntr  24639  neibl  24727  blnei  24728  metss  24734  stdbdmetval  24740  prdsms  24757  blval2  24788  lmmbr  25486  lmmbr2  25487  iscau2  25505  bcthlem1  25552  bcthlem3  25554  bcthlem4  25555  dvn2bss  26157  dvfsumrlim  26258  dvfsumrlim2  26259  cxpexpz  26904  cxpsub  26919  cxpcom  26976  relogbzexp  27013  ltsubs1  28341  1ewlk  30585  1pthon2ve  30634  upgr4cycl4dv4e  30665  konigsbergssiedgwpr  30729  dlwwlknondlwlknonf1o  30845  hvaddsub12  31519  hvaddsubass  31522  hvsubdistr1  31530  hvsubcan  31555  hhssnv  31745  spanunsni  32060  homco1  32282  homulass  32283  hoadddir  32285  hosubdi  32289  hoaddsubass  32296  hosubsub4  32299  lnopmi  32481  adjlnop  32567  mdsymlem5  32888  disjif  33051  disjif2  33054  sigaclfu  34629  signstfvc  35082  bnj544  35403  bnj561  35412  bnj562  35413  bnj594  35421  fineqvnttrclselem3  35649  satfvsuc  35940  satfvsucsuc  35944  clsint2  36948  weiunso  37085  weiunwe  37088  ftc1anclem6  38447  isbnd2  38533  blbnd  38537  isdrngo2  38708  atnem0  40191  hlrelat5N  40274  ltrnel  41012  ltrnat  41013  ltrncnvat  41014  nnproddivdvdsd  42866  dvdsexpnn  43208  jm2.22  43836  jm2.23  43837  dvconstbi  45158  eelT11  45529  eelT12  45531  eelTT1  45532  eelT01  45533  eel0T1  45534  liminfvalxr  46611  grlimprclnbgr  48912  rmfsupp  49303  scmfsupp  49305  dignn0flhalflem2  49546  rrx2vlinest  49671  rrx2linesl  49673