Theorem syl3an3 1164

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3l  1179  3adant3r  1180  syl3an3b  1404  syl3an3br  1407  disji  5132  ovmpox  7585  ovmpoga  7586  wrecseq123  8337  wfrlem14OLD  8360  dif1en  9198  dif1enOLD  9200  domtrfil  9229  ssdomfi2  9234  domnsymfi  9237  sdomdomtrfi  9238  domsdomtrfi  9239  phplem2  9242  php  9244  php3  9246  findcard3  9315  unbnn2  9330  axdc3lem4  10490  axdclem2  10557  gruiin  10847  gruen  10849  divass  11937  ltmul2  12115  xleadd1  13293  xltadd2  13295  xlemul1  13328  xltmul2  13331  elfzo  13697  modcyc2  13943  faclbnd5  14333  relexprel  15074  subcn2  15627  mulcn2  15628  ndvdsp1  16444  gcddiv  16584  lcmneg  16636  lubel  18571  mndpfsupp  18792  gsumccatsn  18868  mulgaddcom  19128  oddvdsi  19580  odcong  19581  odeq  19582  efgsp1  19769  lspsnss  21005  rnglidlrng  21274  lindsmm2  21866  mulmarep1el  22593  mdetunilem4  22636  iuncld  23068  neips  23136  opnneip  23142  comppfsc  23555  hmeof1o2  23786  ordthmeo  23825  ufinffr  23952  elfm3  23973  utop3cls  24275  blcntrps  24437  blcntr  24438  neibl  24529  blnei  24530  metss  24536  stdbdmetval  24542  prdsms  24559  blval2  24590  lmmbr  25305  lmmbr2  25306  iscau2  25324  bcthlem1  25371  bcthlem3  25373  bcthlem4  25374  dvn2bss  25980  dvfsumrlim  26086  dvfsumrlim2  26087  cxpexpz  26723  cxpsub  26738  cxpcom  26795  relogbzexp  26833  sltsub1  28120  1ewlk  30143  1pthon2ve  30182  upgr4cycl4dv4e  30213  konigsbergssiedgwpr  30277  dlwwlknondlwlknonf1o  30393  hvaddsub12  31066  hvaddsubass  31069  hvsubdistr1  31077  hvsubcan  31102  hhssnv  31292  spanunsni  31607  homco1  31829  homulass  31830  hoadddir  31832  hosubdi  31836  hoaddsubass  31843  hosubsub4  31846  lnopmi  32028  adjlnop  32114  mdsymlem5  32435  disjif  32597  disjif2  32600  ind0  33998  sigaclfu  34099  signstfvc  34567  bnj544  34886  bnj561  34895  bnj562  34896  bnj594  34904  swrdrevpfx  35100  satfvsuc  35345  satfvsucsuc  35349  clsint2  36311  weiunso  36448  weiunwe  36451  ftc1anclem6  37684  isbnd2  37769  blbnd  37773  isdrngo2  37944  atnem0  39299  hlrelat5N  39383  ltrnel  40121  ltrnat  40122  ltrncnvat  40123  nnproddivdvdsd  41981  dvdsexpnn  42346  jm2.22  42983  jm2.23  42984  dvconstbi  44329  eelT11  44704  eelT12  44706  eelTT1  44707  eelT01  44708  eel0T1  44709  liminfvalxr  45738  rmfsupp  48217  scmfsupp  48219  dignn0flhalflem2  48465  rrx2vlinest  48590  rrx2linesl  48592