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  5092  ovmpox  7542  ovmpoga  7543  wrecseq123  8292  dif1en  9124  dif1enOLD  9126  domtrfil  9156  ssdomfi2  9161  domnsymfi  9164  sdomdomtrfi  9165  domsdomtrfi  9166  phplem2  9169  php  9171  php3  9173  findcard3  9229  unbnn2  9244  axdc3lem4  10406  axdclem2  10473  gruiin  10763  gruen  10765  divass  11855  ltmul2  12033  xleadd1  13215  xltadd2  13217  xlemul1  13250  xltmul2  13253  elfzo  13622  modcyc2  13869  faclbnd5  14263  relexprel  15005  subcn2  15561  mulcn2  15562  ndvdsp1  16381  gcddiv  16521  lcmneg  16573  lubel  18473  mndpfsupp  18694  gsumccatsn  18770  mulgaddcom  19030  oddvdsi  19478  odcong  19479  odeq  19480  efgsp1  19667  lspsnss  20896  rnglidlrng  21157  lindsmm2  21738  mulmarep1el  22459  mdetunilem4  22502  iuncld  22932  neips  23000  opnneip  23006  comppfsc  23419  hmeof1o2  23650  ordthmeo  23689  ufinffr  23816  elfm3  23837  utop3cls  24139  blcntrps  24300  blcntr  24301  neibl  24389  blnei  24390  metss  24396  stdbdmetval  24402  prdsms  24419  blval2  24450  lmmbr  25158  lmmbr2  25159  iscau2  25177  bcthlem1  25224  bcthlem3  25226  bcthlem4  25227  dvn2bss  25832  dvfsumrlim  25938  dvfsumrlim2  25939  cxpexpz  26576  cxpsub  26591  cxpcom  26648  relogbzexp  26686  sltsub1  27980  1ewlk  30044  1pthon2ve  30083  upgr4cycl4dv4e  30114  konigsbergssiedgwpr  30178  dlwwlknondlwlknonf1o  30294  hvaddsub12  30967  hvaddsubass  30970  hvsubdistr1  30978  hvsubcan  31003  hhssnv  31193  spanunsni  31508  homco1  31730  homulass  31731  hoadddir  31733  hosubdi  31737  hoaddsubass  31744  hosubsub4  31747  lnopmi  31929  adjlnop  32015  mdsymlem5  32336  disjif  32507  disjif2  32510  ind0  32781  sigaclfu  34109  signstfvc  34565  bnj544  34884  bnj561  34893  bnj562  34894  bnj594  34902  swrdrevpfx  35104  satfvsuc  35348  satfvsucsuc  35352  clsint2  36317  weiunso  36454  weiunwe  36457  ftc1anclem6  37692  isbnd2  37777  blbnd  37781  isdrngo2  37952  atnem0  39311  hlrelat5N  39395  ltrnel  40133  ltrnat  40134  ltrncnvat  40135  nnproddivdvdsd  41988  dvdsexpnn  42321  jm2.22  42984  jm2.23  42985  dvconstbi  44323  eelT11  44696  eelT12  44698  eelTT1  44699  eelT01  44700  eel0T1  44701  liminfvalxr  45781  rmfsupp  48361  scmfsupp  48363  dignn0flhalflem2  48605  rrx2vlinest  48730  rrx2linesl  48732