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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant3l  1181  3adant3r  1182  syl3an3b  1407  syl3an3br  1410  disji  5128  ovmpox  7586  ovmpoga  7587  wrecseq123  8339  wfrlem14OLD  8362  dif1en  9200  dif1enOLD  9202  domtrfil  9232  ssdomfi2  9237  domnsymfi  9240  sdomdomtrfi  9241  domsdomtrfi  9242  phplem2  9245  php  9247  php3  9249  findcard3  9318  unbnn2  9333  axdc3lem4  10493  axdclem2  10560  gruiin  10850  gruen  10852  divass  11940  ltmul2  12118  xleadd1  13297  xltadd2  13299  xlemul1  13332  xltmul2  13335  elfzo  13701  modcyc2  13947  faclbnd5  14337  relexprel  15078  subcn2  15631  mulcn2  15632  ndvdsp1  16448  gcddiv  16588  lcmneg  16640  lubel  18559  mndpfsupp  18780  gsumccatsn  18856  mulgaddcom  19116  oddvdsi  19566  odcong  19567  odeq  19568  efgsp1  19755  lspsnss  20988  rnglidlrng  21257  lindsmm2  21849  mulmarep1el  22578  mdetunilem4  22621  iuncld  23053  neips  23121  opnneip  23127  comppfsc  23540  hmeof1o2  23771  ordthmeo  23810  ufinffr  23937  elfm3  23958  utop3cls  24260  blcntrps  24422  blcntr  24423  neibl  24514  blnei  24515  metss  24521  stdbdmetval  24527  prdsms  24544  blval2  24575  lmmbr  25292  lmmbr2  25293  iscau2  25311  bcthlem1  25358  bcthlem3  25360  bcthlem4  25361  dvn2bss  25966  dvfsumrlim  26072  dvfsumrlim2  26073  cxpexpz  26709  cxpsub  26724  cxpcom  26781  relogbzexp  26819  sltsub1  28106  1ewlk  30134  1pthon2ve  30173  upgr4cycl4dv4e  30204  konigsbergssiedgwpr  30268  dlwwlknondlwlknonf1o  30384  hvaddsub12  31057  hvaddsubass  31060  hvsubdistr1  31068  hvsubcan  31093  hhssnv  31283  spanunsni  31598  homco1  31820  homulass  31821  hoadddir  31823  hosubdi  31827  hoaddsubass  31834  hosubsub4  31837  lnopmi  32019  adjlnop  32105  mdsymlem5  32426  disjif  32591  disjif2  32594  ind0  32843  sigaclfu  34120  signstfvc  34589  bnj544  34908  bnj561  34917  bnj562  34918  bnj594  34926  swrdrevpfx  35122  satfvsuc  35366  satfvsucsuc  35370  clsint2  36330  weiunso  36467  weiunwe  36470  ftc1anclem6  37705  isbnd2  37790  blbnd  37794  isdrngo2  37965  atnem0  39319  hlrelat5N  39403  ltrnel  40141  ltrnat  40142  ltrncnvat  40143  nnproddivdvdsd  42001  dvdsexpnn  42368  jm2.22  43007  jm2.23  43008  dvconstbi  44353  eelT11  44727  eelT12  44729  eelTT1  44730  eelT01  44731  eel0T1  44732  liminfvalxr  45798  rmfsupp  48289  scmfsupp  48291  dignn0flhalflem2  48537  rrx2vlinest  48662  rrx2linesl  48664