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  5095  ovmpox  7545  ovmpoga  7546  wrecseq123  8295  dif1en  9130  dif1enOLD  9132  domtrfil  9162  ssdomfi2  9167  domnsymfi  9170  sdomdomtrfi  9171  domsdomtrfi  9172  phplem2  9175  php  9177  php3  9179  findcard3  9236  unbnn2  9251  axdc3lem4  10413  axdclem2  10480  gruiin  10770  gruen  10772  divass  11862  ltmul2  12040  xleadd1  13222  xltadd2  13224  xlemul1  13257  xltmul2  13260  elfzo  13629  modcyc2  13876  faclbnd5  14270  relexprel  15012  subcn2  15568  mulcn2  15569  ndvdsp1  16388  gcddiv  16528  lcmneg  16580  lubel  18480  mndpfsupp  18701  gsumccatsn  18777  mulgaddcom  19037  oddvdsi  19485  odcong  19486  odeq  19487  efgsp1  19674  lspsnss  20903  rnglidlrng  21164  lindsmm2  21745  mulmarep1el  22466  mdetunilem4  22509  iuncld  22939  neips  23007  opnneip  23013  comppfsc  23426  hmeof1o2  23657  ordthmeo  23696  ufinffr  23823  elfm3  23844  utop3cls  24146  blcntrps  24307  blcntr  24308  neibl  24396  blnei  24397  metss  24403  stdbdmetval  24409  prdsms  24426  blval2  24457  lmmbr  25165  lmmbr2  25166  iscau2  25184  bcthlem1  25231  bcthlem3  25233  bcthlem4  25234  dvn2bss  25839  dvfsumrlim  25945  dvfsumrlim2  25946  cxpexpz  26583  cxpsub  26598  cxpcom  26655  relogbzexp  26693  sltsub1  27987  1ewlk  30051  1pthon2ve  30090  upgr4cycl4dv4e  30121  konigsbergssiedgwpr  30185  dlwwlknondlwlknonf1o  30301  hvaddsub12  30974  hvaddsubass  30977  hvsubdistr1  30985  hvsubcan  31010  hhssnv  31200  spanunsni  31515  homco1  31737  homulass  31738  hoadddir  31740  hosubdi  31744  hoaddsubass  31751  hosubsub4  31754  lnopmi  31936  adjlnop  32022  mdsymlem5  32343  disjif  32514  disjif2  32517  ind0  32788  sigaclfu  34116  signstfvc  34572  bnj544  34891  bnj561  34900  bnj562  34901  bnj594  34909  swrdrevpfx  35111  satfvsuc  35355  satfvsucsuc  35359  clsint2  36324  weiunso  36461  weiunwe  36464  ftc1anclem6  37699  isbnd2  37784  blbnd  37788  isdrngo2  37959  atnem0  39318  hlrelat5N  39402  ltrnel  40140  ltrnat  40141  ltrncnvat  40142  nnproddivdvdsd  41995  dvdsexpnn  42328  jm2.22  42991  jm2.23  42992  dvconstbi  44330  eelT11  44703  eelT12  44705  eelTT1  44706  eelT01  44707  eel0T1  44708  liminfvalxr  45788  rmfsupp  48365  scmfsupp  48367  dignn0flhalflem2  48609  rrx2vlinest  48734  rrx2linesl  48736