Theorem syl3an3 1162

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

Syntax hints:   → wi 4   ∧ w3a 1084

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

This theorem is referenced by:  3adant3l  1177  3adant3r  1178  syl3an3b  1402  syl3an3br  1405  disji  5013  ovmpox  7282  ovmpoga  7283  wfrlem14  7951  unbnn2  8759  axdc3lem4  9864  axdclem2  9931  gruiin  10221  gruen  10223  divass  11305  ltmul2  11480  xleadd1  12636  xltadd2  12638  xlemul1  12671  xltmul2  12674  elfzo  13035  modcyc2  13270  faclbnd5  13654  relexprel  14390  subcn2  14943  mulcn2  14944  ndvdsp1  15752  gcddiv  15889  lcmneg  15937  lubel  17724  gsumccatsn  18000  mulgaddcom  18243  oddvdsi  18668  odcong  18669  odeq  18670  efgsp1  18855  lspsnss  19755  lindsmm2  20518  mulmarep1el  21177  mdetunilem4  21220  iuncld  21650  neips  21718  opnneip  21724  comppfsc  22137  hmeof1o2  22368  ordthmeo  22407  ufinffr  22534  elfm3  22555  utop3cls  22857  blcntrps  23019  blcntr  23020  neibl  23108  blnei  23109  metss  23115  stdbdmetval  23121  prdsms  23138  blval2  23169  lmmbr  23862  lmmbr2  23863  iscau2  23881  bcthlem1  23928  bcthlem3  23930  bcthlem4  23931  dvn2bss  24533  dvfsumrlim  24634  dvfsumrlim2  24635  cxpexpz  25258  cxpsub  25273  cxpcom  25328  relogbzexp  25362  1ewlk  27900  1pthon2ve  27939  upgr4cycl4dv4e  27970  konigsbergssiedgwpr  28034  dlwwlknondlwlknonf1o  28150  hvaddsub12  28821  hvaddsubass  28824  hvsubdistr1  28832  hvsubcan  28857  hhssnv  29047  spanunsni  29362  homco1  29584  homulass  29585  hoadddir  29587  hosubdi  29591  hoaddsubass  29598  hosubsub4  29601  lnopmi  29783  adjlnop  29869  mdsymlem5  30190  disjif  30341  disjif2  30344  ind0  31387  sigaclfu  31488  signstfvc  31954  bnj544  32276  bnj561  32285  bnj562  32286  bnj594  32294  swrdrevpfx  32476  satfvsuc  32721  satfvsucsuc  32725  clsint2  33790  ftc1anclem6  35135  isbnd2  35221  blbnd  35225  isdrngo2  35396  atnem0  36614  hlrelat5N  36697  ltrnel  37435  ltrnat  37436  ltrncnvat  37437  nnproddivdvdsd  39289  jm2.22  39936  jm2.23  39937  dvconstbi  41038  eelT11  41413  eelT12  41415  eelTT1  41416  eelT01  41417  eel0T1  41418  liminfvalxr  42425  rmfsupp  44776  mndpfsupp  44778  scmfsupp  44780  dignn0flhalflem2  45030  rrx2vlinest  45155  rrx2linesl  45157