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 1087

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 397  df-3an 1089

This theorem is referenced by:  3adant3l  1180  3adant3r  1181  syl3an3b  1405  syl3an3br  1408  disji  5130  ovmpox  7557  ovmpoga  7558  wrecseq123  8295  wfrlem14OLD  8318  dif1en  9156  dif1enOLD  9158  domtrfil  9191  ssdomfi2  9196  domnsymfi  9199  sdomdomtrfi  9200  domsdomtrfi  9201  phplem2  9204  php  9206  php3  9208  findcard3  9281  unbnn2  9296  axdc3lem4  10444  axdclem2  10511  gruiin  10801  gruen  10803  divass  11886  ltmul2  12061  xleadd1  13230  xltadd2  13232  xlemul1  13265  xltmul2  13268  elfzo  13630  modcyc2  13868  faclbnd5  14254  relexprel  14982  subcn2  15535  mulcn2  15536  ndvdsp1  16350  gcddiv  16489  lcmneg  16536  lubel  18463  gsumccatsn  18720  mulgaddcom  18972  oddvdsi  19410  odcong  19411  odeq  19412  efgsp1  19599  lspsnss  20593  lindsmm2  21375  mulmarep1el  22065  mdetunilem4  22108  iuncld  22540  neips  22608  opnneip  22614  comppfsc  23027  hmeof1o2  23258  ordthmeo  23297  ufinffr  23424  elfm3  23445  utop3cls  23747  blcntrps  23909  blcntr  23910  neibl  24001  blnei  24002  metss  24008  stdbdmetval  24014  prdsms  24031  blval2  24062  lmmbr  24766  lmmbr2  24767  iscau2  24785  bcthlem1  24832  bcthlem3  24834  bcthlem4  24835  dvn2bss  25438  dvfsumrlim  25539  dvfsumrlim2  25540  cxpexpz  26166  cxpsub  26181  cxpcom  26236  relogbzexp  26270  sltsub1  27532  1ewlk  29357  1pthon2ve  29396  upgr4cycl4dv4e  29427  konigsbergssiedgwpr  29491  dlwwlknondlwlknonf1o  29607  hvaddsub12  30278  hvaddsubass  30281  hvsubdistr1  30289  hvsubcan  30314  hhssnv  30504  spanunsni  30819  homco1  31041  homulass  31042  hoadddir  31044  hosubdi  31048  hoaddsubass  31055  hosubsub4  31058  lnopmi  31240  adjlnop  31326  mdsymlem5  31647  disjif  31796  disjif2  31799  ind0  33004  sigaclfu  33105  signstfvc  33573  bnj544  33893  bnj561  33902  bnj562  33903  bnj594  33911  swrdrevpfx  34095  satfvsuc  34340  satfvsucsuc  34344  clsint2  35202  ftc1anclem6  36554  isbnd2  36639  blbnd  36643  isdrngo2  36814  atnem0  38176  hlrelat5N  38260  ltrnel  38998  ltrnat  38999  ltrncnvat  39000  nnproddivdvdsd  40854  dvdsexpnn  41226  jm2.22  41719  jm2.23  41720  dvconstbi  43078  eelT11  43453  eelT12  43455  eelTT1  43456  eelT01  43457  eel0T1  43458  liminfvalxr  44485  rnglidlrng  46740  rmfsupp  47003  mndpfsupp  47005  scmfsupp  47007  dignn0flhalflem2  47255  rrx2vlinest  47380  rrx2linesl  47382