Theorem syl3an3 1177

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  3adant3l  1193  3adant3r  1194  syl3an3b  1423  syl3an3br  1426  disji  5082  ovmpox  7544  ovmpoga  7545  wrecseq123  8288  dif1en  9124  domtrfil  9154  ssdomfi2  9159  domnsymfi  9162  sdomdomtrfi  9163  domsdomtrfi  9164  phplem2  9167  php  9169  php3  9171  findcard3  9221  unbnn2  9235  axdc3lem4  10404  axdclem2  10471  gruiin  10762  gruen  10764  divass  11857  ltmul2  12036  ind0  12199  xleadd1  13252  xltadd2  13254  xlemul1  13287  xltmul2  13290  elfzo  13660  modcyc2  13911  faclbnd5  14305  relexprel  15046  subcn2  15613  mulcn2  15614  ndvdsp1  16436  gcddiv  16576  lcmneg  16628  lubel  18537  mndpfsupp  18792  gsumccatsn  18868  mulgaddcom  19131  oddvdsi  19579  odcong  19580  odeq  19581  efgsp1  19768  lspsnss  21045  rnglidlrng  21305  lindsmm2  21869  mulmarep1el  22620  mdetunilem4  22663  iuncld  23093  neips  23161  opnneip  23167  comppfsc  23580  hmeof1o2  23811  ordthmeo  23850  ufinffr  23977  elfm3  23998  utop3cls  24299  blcntrps  24460  blcntr  24461  neibl  24549  blnei  24550  metss  24556  stdbdmetval  24562  prdsms  24579  blval2  24610  lmmbr  25308  lmmbr2  25309  iscau2  25327  bcthlem1  25374  bcthlem3  25376  bcthlem4  25377  dvn2bss  25980  dvfsumrlim  26081  dvfsumrlim2  26082  cxpexpz  26720  cxpsub  26735  cxpcom  26792  relogbzexp  26829  ltsubs1  28157  1ewlk  30274  1pthon2ve  30313  upgr4cycl4dv4e  30344  konigsbergssiedgwpr  30408  dlwwlknondlwlknonf1o  30524  hvaddsub12  31198  hvaddsubass  31201  hvsubdistr1  31209  hvsubcan  31234  hhssnv  31424  spanunsni  31739  homco1  31961  homulass  31962  hoadddir  31964  hosubdi  31968  hoaddsubass  31975  hosubsub4  31978  lnopmi  32160  adjlnop  32246  mdsymlem5  32567  disjif  32738  disjif2  32741  sigaclfu  34377  signstfvc  34829  bnj544  35150  bnj561  35159  bnj562  35160  bnj594  35168  fineqvnttrclselem3  35380  swrdrevpfx  35428  satfvsuc  35672  satfvsucsuc  35676  clsint2  36650  weiunso  36787  weiunwe  36790  ftc1anclem6  38158  isbnd2  38243  blbnd  38247  isdrngo2  38418  atnem0  39903  hlrelat5N  39986  ltrnel  40724  ltrnat  40725  ltrncnvat  40726  nnproddivdvdsd  42578  dvdsexpnn  42903  jm2.22  43533  jm2.23  43534  dvconstbi  44871  eelT11  45243  eelT12  45245  eelTT1  45246  eelT01  45247  eel0T1  45248  liminfvalxr  46318  grlimprclnbgr  48579  rmfsupp  48956  scmfsupp  48958  dignn0flhalflem2  49199  rrx2vlinest  49324  rrx2linesl  49326