Theorem syl3an3 1161

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3l  1176  3adant3r  1177  syl3an3b  1401  syl3an3br  1404  disji  5042  ovmpox  7297  ovmpoga  7298  wfrlem14  7962  unbnn2  8769  axdc3lem4  9869  axdclem2  9936  gruiin  10226  gruen  10228  divass  11310  ltmul2  11485  xleadd1  12642  xltadd2  12644  xlemul1  12677  xltmul2  12680  elfzo  13034  modcyc2  13269  faclbnd5  13652  relexprel  14392  subcn2  14945  mulcn2  14946  ndvdsp1  15756  gcddiv  15893  lcmneg  15941  lubel  17726  gsumccatsn  18002  mulgaddcom  18245  oddvdsi  18670  odcong  18671  odeq  18672  efgsp1  18857  lspsnss  19756  lindsmm2  20967  mulmarep1el  21175  mdetunilem4  21218  iuncld  21647  neips  21715  opnneip  21721  comppfsc  22134  hmeof1o2  22365  ordthmeo  22404  ufinffr  22531  elfm3  22552  utop3cls  22854  blcntrps  23016  blcntr  23017  neibl  23105  blnei  23106  metss  23112  stdbdmetval  23118  prdsms  23135  blval2  23166  lmmbr  23855  lmmbr2  23856  iscau2  23874  bcthlem1  23921  bcthlem3  23923  bcthlem4  23924  dvn2bss  24521  dvfsumrlim  24622  dvfsumrlim2  24623  cxpexpz  25244  cxpsub  25259  cxpcom  25314  relogbzexp  25348  1ewlk  27888  1pthon2ve  27927  upgr4cycl4dv4e  27958  konigsbergssiedgwpr  28022  dlwwlknondlwlknonf1o  28138  hvaddsub12  28809  hvaddsubass  28812  hvsubdistr1  28820  hvsubcan  28845  hhssnv  29035  spanunsni  29350  homco1  29572  homulass  29573  hoadddir  29575  hosubdi  29579  hoaddsubass  29586  hosubsub4  29589  lnopmi  29771  adjlnop  29857  mdsymlem5  30178  disjif  30322  disjif2  30325  ind0  31272  sigaclfu  31373  signstfvc  31839  bnj544  32161  bnj561  32170  bnj562  32171  bnj594  32179  swrdrevpfx  32358  satfvsuc  32603  satfvsucsuc  32607  clsint2  33672  ftc1anclem6  34966  isbnd2  35055  blbnd  35059  isdrngo2  35230  atnem0  36448  hlrelat5N  36531  ltrnel  37269  ltrnat  37270  ltrncnvat  37271  jm2.22  39585  jm2.23  39586  dvconstbi  40659  eelT11  41034  eelT12  41036  eelTT1  41037  eelT01  41038  eel0T1  41039  liminfvalxr  42056  rmfsupp  44415  mndpfsupp  44417  scmfsupp  44419  dignn0flhalflem2  44669  rrx2vlinest  44721  rrx2linesl  44723