MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an2 Structured version   Visualization version   GIF version

Theorem syl3an2 1165
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
StepHypRef Expression
1 syl3an2.1 . . 3 (𝜑𝜒)
213anim2i 1154 . 2 ((𝜓𝜑𝜃) → (𝜓𝜒𝜃))
3 syl3an2.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff setvar class
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3adant2l  1179  3adant2r  1180  syl3an2b  1406  syl3an2br  1409  fviunfun  7969  odi  8617  omass  8618  nndi  8661  nnmass  8662  omabslem  8688  domtrfil  9232  domnsymfi  9240  sdomdomtrfi  9241  domsdomtrfi  9242  php  9247  php3  9249  f1finf1o  9305  findcard3  9318  winainf  10734  divsubdir  11961  divdiv32  11975  ltdiv2  12154  peano2uz  12943  irrmul  13016  supxrunb1  13361  fzoshftral  13823  ltdifltdiv  13874  axdc4uzlem  14024  expdiv  14154  bcval5  14357  rediv  15170  imdiv  15177  absdiflt  15356  absdifle  15357  iseraltlem3  15720  retancl  16178  tanneg  16184  lcmgcdeq  16649  prmdvdsexpb  16753  dvdsprmpweqnn  16923  mulgaddcomlem  19115  mulginvcom  19117  pmtrfb  19483  lspssp  20986  mdetunilem7  22624  m2detleiblem3  22635  m2detleiblem4  22636  pmatcollpw  22787  pmatcollpwscmat  22797  chpmatply1  22838  chfacfscmulgsum  22866  chfacfpmmulcl  22867  chfacfpmmul0  22868  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadurid  22873  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmidgsum2  22885  islp2  23153  fmfg  23957  fmufil  23967  flffbas  24003  lmflf  24013  uffcfflf  24047  blres  24441  ncvsge0  25187  caucfil  25317  cmetcusp1  25387  deg1mul3  26155  quotval  26334  sltonold  28283  cusgr3vnbpr  29453  clwwlkinwwlk  30059  nvsge0  30683  hvsubass  31063  hvsubdistr2  31069  hvsubcan  31093  his2sub  31111  chlub  31528  spanunsni  31598  homco1  31820  homulass  31821  cnlnadjlem2  32087  adjmul  32111  chirredlem2  32410  atmd2  32419  mdsymlem5  32426  f1resrcmplf1dlem  35100  revpfxsfxrev  35121  climuzcnv  35676  pibt2  37418  f1ocan2fv  37734  isdrngo2  37965  atncvrN  39316  cvlatcvr1  39342  eluzrabdioph  42817  iocmbl  43225  rp-isfinite6  43531  ismnushort  44320  dvconstbi  44353  eelT11  44727  eelT12  44729  eelTT1  44730  eel0T1  44732  nn0digval  48521  dignn0flhalf  48539  sinhpcosh  49259  reseccl  49272  recsccl  49273  recotcl  49274  onetansqsecsq  49280
  Copyright terms: Public domain W3C validator