Theorem syl3an2 1164

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syl3an2.1	⊢ (𝜑 → 𝜒)
syl3an2.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	3anim2i 1153	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an2.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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adant2l  1178  3adant2r  1179  syl3an2b  1404  syl3an2br  1407  fviunfun  7930  odi  8578  omass  8579  nndi  8622  nnmass  8623  omabslem  8648  domtrfil  9194  domnsymfi  9202  sdomdomtrfi  9203  domsdomtrfi  9204  php  9209  php3  9211  f1finf1o  9270  findcard3  9284  winainf  10688  divsubdir  11907  divdiv32  11921  ltdiv2  12099  peano2uz  12884  irrmul  12957  supxrunb1  13297  fzoshftral  13748  ltdifltdiv  13798  axdc4uzlem  13947  expdiv  14078  bcval5  14277  rediv  15077  imdiv  15084  absdiflt  15263  absdifle  15264  iseraltlem3  15629  retancl  16084  tanneg  16090  lcmgcdeq  16548  prmdvdsexpb  16652  dvdsprmpweqnn  16817  mulgaddcomlem  18976  mulginvcom  18978  pmtrfb  19332  lspssp  20598  mdetunilem7  22119  m2detleiblem3  22130  m2detleiblem4  22131  pmatcollpw  22282  pmatcollpwscmat  22292  chpmatply1  22333  chfacfscmulgsum  22361  chfacfpmmulcl  22362  chfacfpmmul0  22363  chfacfpmmulgsum  22365  chfacfpmmulgsum2  22366  cayhamlem1  22367  cpmadurid  22368  cpmadugsumlemC  22376  cpmadugsumlemF  22377  cpmadugsumfi  22378  cpmidgsum2  22380  islp2  22648  fmfg  23452  fmufil  23462  flffbas  23498  lmflf  23508  uffcfflf  23542  blres  23936  ncvsge0  24669  caucfil  24799  cmetcusp1  24869  deg1mul3  25632  quotval  25804  cusgr3vnbpr  28690  clwwlkinwwlk  29290  nvsge0  29912  hvsubass  30292  hvsubdistr2  30298  hvsubcan  30322  his2sub  30340  chlub  30757  spanunsni  30827  homco1  31049  homulass  31050  cnlnadjlem2  31316  adjmul  31340  chirredlem2  31639  atmd2  31648  mdsymlem5  31655  f1resrcmplf1dlem  34084  revpfxsfxrev  34101  climuzcnv  34651  pibt2  36293  f1ocan2fv  36590  isdrngo2  36821  atncvrN  38180  cvlatcvr1  38206  eluzrabdioph  41534  iocmbl  41952  rp-isfinite6  42259  ismnushort  43050  dvconstbi  43083  eelT11  43458  eelT12  43460  eelTT1  43461  eel0T1  43463  nn0digval  47276  dignn0flhalf  47294  sinhpcosh  47775  reseccl  47788  recsccl  47789  recotcl  47790  onetansqsecsq  47796