Theorem syl3an3 1161

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3l  1176  3adant3r  1177  syl3an3b  1401  syl3an3br  1404  disji  5051  ovmpox  7305  ovmpoga  7306  wfrlem14  7970  unbnn2  8777  axdc3lem4  9877  axdclem2  9944  gruiin  10234  gruen  10236  divass  11318  ltmul2  11493  xleadd1  12651  xltadd2  12653  xlemul1  12686  xltmul2  12689  elfzo  13043  modcyc2  13278  faclbnd5  13661  relexprel  14400  subcn2  14953  mulcn2  14954  ndvdsp1  15764  gcddiv  15901  lcmneg  15949  lubel  17734  gsumccatsn  18010  mulgaddcom  18253  oddvdsi  18678  odcong  18679  odeq  18680  efgsp1  18865  lspsnss  19764  lindsmm2  20975  mulmarep1el  21183  mdetunilem4  21226  iuncld  21655  neips  21723  opnneip  21729  comppfsc  22142  hmeof1o2  22373  ordthmeo  22412  ufinffr  22539  elfm3  22560  utop3cls  22862  blcntrps  23024  blcntr  23025  neibl  23113  blnei  23114  metss  23120  stdbdmetval  23126  prdsms  23143  blval2  23174  lmmbr  23863  lmmbr2  23864  iscau2  23882  bcthlem1  23929  bcthlem3  23931  bcthlem4  23932  dvn2bss  24529  dvfsumrlim  24630  dvfsumrlim2  24631  cxpexpz  25252  cxpsub  25267  cxpcom  25322  relogbzexp  25356  1ewlk  27896  1pthon2ve  27935  upgr4cycl4dv4e  27966  konigsbergssiedgwpr  28030  dlwwlknondlwlknonf1o  28146  hvaddsub12  28817  hvaddsubass  28820  hvsubdistr1  28828  hvsubcan  28853  hhssnv  29043  spanunsni  29358  homco1  29580  homulass  29581  hoadddir  29583  hosubdi  29587  hoaddsubass  29594  hosubsub4  29597  lnopmi  29779  adjlnop  29865  mdsymlem5  30186  disjif  30330  disjif2  30333  ind0  31279  sigaclfu  31380  signstfvc  31846  bnj544  32168  bnj561  32177  bnj562  32178  bnj594  32186  swrdrevpfx  32365  satfvsuc  32610  satfvsucsuc  32614  clsint2  33679  ftc1anclem6  34974  isbnd2  35063  blbnd  35067  isdrngo2  35238  atnem0  36456  hlrelat5N  36539  ltrnel  37277  ltrnat  37278  ltrncnvat  37279  jm2.22  39599  jm2.23  39600  dvconstbi  40673  eelT11  41048  eelT12  41050  eelTT1  41051  eelT01  41052  eel0T1  41053  liminfvalxr  42071  rmfsupp  44429  mndpfsupp  44431  scmfsupp  44433  dignn0flhalflem2  44683  rrx2vlinest  44735  rrx2linesl  44737