Theorem syl3an3 1166

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 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3adant3l  1186  3adant3r  1188  syl3an3b  1473  syl3an3br  1476  disji  4873  ovmpt2x  7068  ovmpt2ga  7069  wfrlem14  7713  unbnn2  8507  axdc3lem4  9612  axdclem2  9679  gruiin  9969  gruen  9971  divass  11053  ltmul2  11230  xleadd1  12401  xltadd2  12403  xlemul1  12436  xltmul2  12439  elfzo  12795  modcyc2  13029  faclbnd5  13407  relexprel  14190  subcn2  14737  mulcn2  14738  ndvdsp1  15545  gcddiv  15678  lcmneg  15726  lubel  17512  gsumccatsn  17770  mulgaddcom  17954  oddvdsi  18355  odcong  18356  odeq  18357  efgsp1  18538  lspsnss  19389  lindsmm2  20576  mulmarep1el  20787  mdetunilem4  20830  iuncld  21261  neips  21329  opnneip  21335  comppfsc  21748  hmeof1o2  21979  ordthmeo  22018  ufinffr  22145  elfm3  22166  utop3cls  22467  blcntrps  22629  blcntr  22630  neibl  22718  blnei  22719  metss  22725  stdbdmetval  22731  prdsms  22748  blval2  22779  lmmbr  23468  lmmbr2  23469  iscau2  23487  bcthlem1  23534  bcthlem3  23536  bcthlem4  23537  dvn2bss  24134  dvfsumrlim  24235  dvfsumrlim2  24236  cxpexpz  24854  cxpsub  24869  cxpcom  24924  relogbzexp  24958  upgr4cycl4dv4e  27592  konigsbergssiedgwpr  27659  dlwwlknondlwlknonf1o  27795  dlwwlknondlwlknonf1oOLD  27796  hvaddsub12  28471  hvaddsubass  28474  hvsubdistr1  28482  hvsubcan  28507  hhssnv  28697  spanunsni  29014  homco1  29236  homulass  29237  hoadddir  29239  hosubdi  29243  hoaddsubass  29250  hosubsub4  29253  lnopmi  29435  adjlnop  29521  mdsymlem5  29842  disjif  29958  disjif2  29961  ind0  30682  sigaclfu  30784  bnj544  31567  bnj561  31576  bnj562  31577  bnj594  31585  clsint2  32916  ftc1anclem6  34120  isbnd2  34211  blbnd  34215  isdrngo2  34386  atnem0  35477  hlrelat5N  35560  ltrnel  36298  ltrnat  36299  ltrncnvat  36300  jm2.22  38531  jm2.23  38532  dvconstbi  39499  eelT11  39886  eelT12  39888  eelTT1  39889  eelT01  39890  eel0T1  39891  liminfvalxr  40933  rmfsupp  43180  mndpfsupp  43182  scmfsupp  43184  dignn0flhalflem2  43435  rrx2vlinest  43487  rrx2linesl  43489