Theorem syl3an3 1183

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  3adant3l  1199  3adant3r  1200  syl3an3b  1432  syl3an3br  1435  disji  5095  ovmpox  7565  ovmpoga  7566  wrecseq123  8311  dif1en  9147  domtrfil  9177  ssdomfi2  9182  domnsymfi  9185  sdomdomtrfi  9186  domsdomtrfi  9187  phplem2  9190  php  9192  php3  9194  findcard3  9244  unbnn2  9258  axdc3lem4  10438  axdclem2  10505  gruiin  10796  gruen  10798  divass  11891  ltmul2  12067  ind0  12229  xleadd1  13282  xltadd2  13284  xlemul1  13317  xltmul2  13320  elfzo  13691  modcyc2  13942  faclbnd5  14336  relexprel  15078  subcn2  15648  mulcn2  15649  ndvdsp1  16470  gcddiv  16610  lcmneg  16662  lubel  18571  mndpfsupp  18826  gsumccatsn  18903  mulgaddcom  19165  oddvdsi  19619  odcong  19620  odeq  19621  efgsp1  19808  lspsnss  21092  rnglidlrng  21362  lindsmm2  21960  mulmarep1el  22710  mdetunilem4  22753  iuncld  23183  neips  23251  opnneip  23257  comppfsc  23670  hmeof1o2  23901  ordthmeo  23940  ufinffr  24067  elfm3  24088  utop3cls  24389  blcntrps  24550  blcntr  24551  neibl  24639  blnei  24640  metss  24646  stdbdmetval  24652  prdsms  24669  blval2  24700  lmmbr  25398  lmmbr2  25399  iscau2  25417  bcthlem1  25464  bcthlem3  25466  bcthlem4  25467  dvn2bss  26070  dvfsumrlim  26171  dvfsumrlim2  26172  cxpexpz  26813  cxpsub  26828  cxpcom  26885  relogbzexp  26922  ltsubs1  28250  1ewlk  30447  1pthon2ve  30486  upgr4cycl4dv4e  30517  konigsbergssiedgwpr  30581  dlwwlknondlwlknonf1o  30697  hvaddsub12  31371  hvaddsubass  31374  hvsubdistr1  31382  hvsubcan  31407  hhssnv  31597  spanunsni  31912  homco1  32134  homulass  32135  hoadddir  32137  hosubdi  32141  hoaddsubass  32148  hosubsub4  32151  lnopmi  32333  adjlnop  32419  mdsymlem5  32740  disjif  32904  disjif2  32907  sigaclfu  34490  signstfvc  34942  bnj544  35263  bnj561  35272  bnj562  35273  bnj594  35281  fineqvnttrclselem3  35517  swrdrevpfx  35589  satfvsuc  35834  satfvsucsuc  35838  clsint2  36821  weiunso  36958  weiunwe  36961  ftc1anclem6  38330  isbnd2  38415  blbnd  38419  isdrngo2  38590  atnem0  40073  hlrelat5N  40156  ltrnel  40894  ltrnat  40895  ltrncnvat  40896  nnproddivdvdsd  42748  dvdsexpnn  43075  jm2.22  43705  jm2.23  43706  dvconstbi  45027  eelT11  45398  eelT12  45400  eelTT1  45401  eelT01  45402  eel0T1  45403  liminfvalxr  46480  grlimprclnbgr  48744  rmfsupp  49136  scmfsupp  49138  dignn0flhalflem2  49379  rrx2vlinest  49504  rrx2linesl  49506