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 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adant2l  1197  3adant2r  1198  syl3an2b  1431  syl3an2br  1434  fviunfun  7943  odi  8565  omass  8566  nndi  8610  nnmass  8611  omabslem  8637  domtrfil  9177  domnsymfi  9185  sdomdomtrfi  9186  domsdomtrfi  9187  php  9192  php3  9194  f1finf1o  9234  findcard3  9244  winainf  10680  divsubdir  11909  divdiv32  11924  ltdiv2  12102  peano2uz  12926  irrmul  12999  supxrunb1  13346  fzoshftral  13818  ltdifltdiv  13869  axdc4uzlem  14021  expdiv  14151  bcval5  14356  rediv  15184  imdiv  15191  absdiflt  15371  absdifle  15372  iseraltlem3  15737  retancl  16199  tanneg  16205  difmod0  16346  lcmgcdeq  16671  prmdvdsexpb  16776  dvdsprmpweqnn  16946  mulgaddcomlem  19164  mulginvcom  19166  pmtrfb  19536  lspssp  21090  mdetunilem7  22756  m2detleiblem3  22767  m2detleiblem4  22768  pmatcollpw  22919  pmatcollpwscmat  22929  chpmatply1  22970  chfacfscmulgsum  22998  chfacfpmmulcl  22999  chfacfpmmul0  23000  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadurid  23005  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cpmadugsumfi  23015  cpmidgsum2  23017  islp2  23283  fmfg  24087  fmufil  24097  flffbas  24133  lmflf  24143  uffcfflf  24177  blres  24569  ncvsge0  25293  caucfil  25423  cmetcusp1  25493  deg1mul3  26254  quotval  26434  ltonold  28435  cusgr3vnbpr  29767  clwwlkinwwlk  30372  nvsge0  30997  hvsubass  31377  hvsubdistr2  31383  hvsubcan  31407  his2sub  31425  chlub  31842  spanunsni  31912  homco1  32134  homulass  32135  cnlnadjlem2  32401  adjmul  32425  chirredlem2  32724  atmd2  32733  mdsymlem5  32740  f1resrcmplf1dlem  35455  revpfxsfxrev  35588  climuzcnv  36144  pibt2  38044  f1ocan2fv  38359  isdrngo2  38590  atncvrN  40070  cvlatcvr1  40096  eluzrabdioph  43516  iocmbl  43923  rp-isfinite6  44227  ismnushort  44994  dvconstbi  45027  eelT11  45398  eelT12  45400  eelTT1  45401  eel0T1  45403  nn0digval  49363  dignn0flhalf  49381  sinhpcosh  50501  reseccl  50514  recsccl  50515  recotcl  50516  onetansqsecsq  50522