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  1182  3adant3r  1183  syl3an3b  1408  syl3an3br  1411  disji  5085  ovmpox  7521  ovmpoga  7522  wrecseq123  8265  dif1en  9098  domtrfil  9128  ssdomfi2  9133  domnsymfi  9136  sdomdomtrfi  9137  domsdomtrfi  9138  phplem2  9141  php  9143  php3  9145  findcard3  9195  unbnn2  9209  axdc3lem4  10375  axdclem2  10442  gruiin  10733  gruen  10735  divass  11826  ltmul2  12004  xleadd1  13182  xltadd2  13184  xlemul1  13217  xltmul2  13220  elfzo  13589  modcyc2  13839  faclbnd5  14233  relexprel  14974  subcn2  15530  mulcn2  15531  ndvdsp1  16350  gcddiv  16490  lcmneg  16542  lubel  18449  mndpfsupp  18704  gsumccatsn  18780  mulgaddcom  19040  oddvdsi  19489  odcong  19490  odeq  19491  efgsp1  19678  lspsnss  20953  rnglidlrng  21214  lindsmm2  21796  mulmarep1el  22528  mdetunilem4  22571  iuncld  23001  neips  23069  opnneip  23075  comppfsc  23488  hmeof1o2  23719  ordthmeo  23758  ufinffr  23885  elfm3  23906  utop3cls  24207  blcntrps  24368  blcntr  24369  neibl  24457  blnei  24458  metss  24464  stdbdmetval  24470  prdsms  24487  blval2  24518  lmmbr  25226  lmmbr2  25227  iscau2  25245  bcthlem1  25292  bcthlem3  25294  bcthlem4  25295  dvn2bss  25900  dvfsumrlim  26006  dvfsumrlim2  26007  cxpexpz  26644  cxpsub  26659  cxpcom  26716  relogbzexp  26754  ltsubs1  28084  1ewlk  30202  1pthon2ve  30241  upgr4cycl4dv4e  30272  konigsbergssiedgwpr  30336  dlwwlknondlwlknonf1o  30452  hvaddsub12  31125  hvaddsubass  31128  hvsubdistr1  31136  hvsubcan  31161  hhssnv  31351  spanunsni  31666  homco1  31888  homulass  31889  hoadddir  31891  hosubdi  31895  hoaddsubass  31902  hosubsub4  31905  lnopmi  32087  adjlnop  32173  mdsymlem5  32494  disjif  32664  disjif2  32667  ind0  32947  sigaclfu  34296  signstfvc  34751  bnj544  35069  bnj561  35078  bnj562  35079  bnj594  35087  fineqvnttrclselem3  35298  swrdrevpfx  35330  satfvsuc  35574  satfvsucsuc  35578  clsint2  36542  weiunso  36679  weiunwe  36682  ftc1anclem6  37946  isbnd2  38031  blbnd  38035  isdrngo2  38206  atnem0  39691  hlrelat5N  39774  ltrnel  40512  ltrnat  40513  ltrncnvat  40514  nnproddivdvdsd  42367  dvdsexpnn  42700  jm2.22  43349  jm2.23  43350  dvconstbi  44687  eelT11  45059  eelT12  45061  eelTT1  45062  eelT01  45063  eel0T1  45064  liminfvalxr  46138  grlimprclnbgr  48353  rmfsupp  48730  scmfsupp  48732  dignn0flhalflem2  48973  rrx2vlinest  49098  rrx2linesl  49100