Theorem syl3an3 1163

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3adant3l  1178  3adant3r  1179  syl3an3b  1403  syl3an3br  1406  disji  5053  ovmpox  7404  ovmpoga  7405  wrecseq123  8101  wfrlem14OLD  8124  dif1en  8907  unbnn2  9001  axdc3lem4  10140  axdclem2  10207  gruiin  10497  gruen  10499  divass  11581  ltmul2  11756  xleadd1  12918  xltadd2  12920  xlemul1  12953  xltmul2  12956  elfzo  13318  modcyc2  13555  faclbnd5  13940  relexprel  14678  subcn2  15232  mulcn2  15233  ndvdsp1  16048  gcddiv  16187  lcmneg  16236  lubel  18147  gsumccatsn  18397  mulgaddcom  18642  oddvdsi  19071  odcong  19072  odeq  19073  efgsp1  19258  lspsnss  20167  lindsmm2  20946  mulmarep1el  21629  mdetunilem4  21672  iuncld  22104  neips  22172  opnneip  22178  comppfsc  22591  hmeof1o2  22822  ordthmeo  22861  ufinffr  22988  elfm3  23009  utop3cls  23311  blcntrps  23473  blcntr  23474  neibl  23563  blnei  23564  metss  23570  stdbdmetval  23576  prdsms  23593  blval2  23624  lmmbr  24327  lmmbr2  24328  iscau2  24346  bcthlem1  24393  bcthlem3  24395  bcthlem4  24396  dvn2bss  24999  dvfsumrlim  25100  dvfsumrlim2  25101  cxpexpz  25727  cxpsub  25742  cxpcom  25797  relogbzexp  25831  1ewlk  28380  1pthon2ve  28419  upgr4cycl4dv4e  28450  konigsbergssiedgwpr  28514  dlwwlknondlwlknonf1o  28630  hvaddsub12  29301  hvaddsubass  29304  hvsubdistr1  29312  hvsubcan  29337  hhssnv  29527  spanunsni  29842  homco1  30064  homulass  30065  hoadddir  30067  hosubdi  30071  hoaddsubass  30078  hosubsub4  30081  lnopmi  30263  adjlnop  30349  mdsymlem5  30670  disjif  30818  disjif2  30821  ind0  31886  sigaclfu  31987  signstfvc  32453  bnj544  32774  bnj561  32783  bnj562  32784  bnj594  32792  swrdrevpfx  32978  satfvsuc  33223  satfvsucsuc  33227  clsint2  34445  ftc1anclem6  35782  isbnd2  35868  blbnd  35872  isdrngo2  36043  atnem0  37259  hlrelat5N  37342  ltrnel  38080  ltrnat  38081  ltrncnvat  38082  nnproddivdvdsd  39937  dvdsexpnn  40261  jm2.22  40733  jm2.23  40734  dvconstbi  41841  eelT11  42216  eelT12  42218  eelTT1  42219  eelT01  42220  eel0T1  42221  liminfvalxr  43214  rmfsupp  45598  mndpfsupp  45600  scmfsupp  45602  dignn0flhalflem2  45850  rrx2vlinest  45975  rrx2linesl  45977