Theorem syl3an2 1182

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant2l  1197  3adant2r  1198  syl3an2b  1431  syl3an2br  1434  f1resrcmplf1dlem  7274  fviunfun  7944  odi  8566  omass  8567  nndi  8611  nnmass  8612  omabslem  8638  domtrfil  9179  domnsymfi  9187  sdomdomtrfi  9188  domsdomtrfi  9189  php  9194  php3  9196  f1finf1o  9236  findcard3  9246  winainf  10690  divsubdir  11919  divdiv32  11934  ltdiv2  12112  peano2uz  12936  irrmul  13009  supxrunb1  13356  fzoshftral  13828  ltdifltdiv  13880  axdc4uzlem  14032  expdiv  14162  bcval5  14367  revpfxsfxrev  14822  rediv  15201  imdiv  15208  absdiflt  15388  absdifle  15389  iseraltlem3  15754  retancl  16215  tanneg  16221  difmod0  16362  lcmgcdeq  16687  prmdvdsexpb  16792  dvdsprmpweqnn  16962  mulgaddcomlem  19186  mulginvcom  19188  pmtrfb  19558  isdrng3lem2  20881  lspssp  21138  mdetunilem7  22804  m2detleiblem3  22815  m2detleiblem4  22816  pmatcollpw  22967  pmatcollpwscmat  22977  chpmatply1  23018  chfacfscmulgsum  23046  chfacfpmmulcl  23047  chfacfpmmul0  23048  chfacfpmmulgsum  23050  chfacfpmmulgsum2  23051  cayhamlem1  23052  cpmadurid  23053  cpmadugsumlemC  23061  cpmadugsumlemF  23062  cpmadugsumfi  23063  cpmidgsum2  23065  islp2  23331  fmfg  24135  fmufil  24145  flffbas  24181  lmflf  24191  uffcfflf  24225  blres  24617  ncvsge0  25341  caucfil  25471  cmetcusp1  25541  deg1mul3  26302  quotval  26482  ltonold  28483  cusgr3vnbpr  29815  clwwlkinwwlk  30420  nvsge0  31045  hvsubass  31425  hvsubdistr2  31431  hvsubcan  31455  his2sub  31473  chlub  31890  spanunsni  31960  homco1  32182  homulass  32183  cnlnadjlem2  32449  adjmul  32473  chirredlem2  32772  atmd2  32781  mdsymlem5  32788  climuzcnv  36176  pibt2  38096  f1ocan2fv  38411  isdrngo2  38642  atncvrN  40122  cvlatcvr1  40148  eluzrabdioph  43566  iocmbl  43973  rp-isfinite6  44277  ismnushort  45044  dvconstbi  45077  eelT11  45448  eelT12  45450  eelTT1  45451  eel0T1  45453  nn0digval  49413  dignn0flhalf  49431  sinhpcosh  50551  reseccl  50564  recsccl  50565  recotcl  50566  onetansqsecsq  50572