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

Theorem syl3an2 1161
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 1150 . 2 ((𝜓𝜑𝜃) → (𝜓𝜒𝜃))
3 syl3an2.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 400  df-3an 1086
This theorem is referenced by:  3adant2l  1175  3adant2r  1176  syl3an2b  1401  syl3an2br  1404  fviunfun  7632  odi  8192  omass  8193  nndi  8236  nnmass  8237  omabslem  8260  winainf  10109  divsubdir  11327  divdiv32  11341  ltdiv2  11519  peano2uz  12293  irrmul  12365  supxrunb1  12704  fzoshftral  13153  ltdifltdiv  13203  axdc4uzlem  13350  expdiv  13480  bcval5  13678  ccats1val1OLD  13977  rediv  14485  imdiv  14492  absdiflt  14672  absdifle  14673  iseraltlem3  15035  retancl  15490  tanneg  15496  lcmgcdeq  15949  prmdvdsexpb  16053  dvdsprmpweqnn  16214  mulgaddcomlem  18245  mulginvcom  18247  pmtrfb  18588  lspssp  19756  mdetunilem7  21226  m2detleiblem3  21237  m2detleiblem4  21238  pmatcollpw  21389  pmatcollpwscmat  21399  chpmatply1  21440  chfacfscmulgsum  21468  chfacfpmmulcl  21469  chfacfpmmul0  21470  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadurid  21475  cpmadugsumlemC  21483  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmidgsum2  21487  islp2  21753  fmfg  22557  fmufil  22567  flffbas  22603  lmflf  22613  uffcfflf  22647  blres  23041  ncvsge0  23761  caucfil  23890  cmetcusp1  23960  deg1mul3  24719  quotval  24891  cusgr3vnbpr  27229  clwwlkinwwlk  27828  nvsge0  28450  hvsubass  28830  hvsubdistr2  28836  hvsubcan  28860  his2sub  28878  chlub  29295  spanunsni  29365  homco1  29587  homulass  29588  cnlnadjlem2  29854  adjmul  29878  chirredlem2  30177  atmd2  30186  mdsymlem5  30193  f1resrcmplf1dlem  32467  revpfxsfxrev  32470  climuzcnv  33022  pibt2  34829  f1ocan2fv  35158  isdrngo2  35389  atncvrN  36604  cvlatcvr1  36630  eluzrabdioph  39734  iocmbl  40150  rp-isfinite6  40213  dvconstbi  41025  eelT11  41400  eelT12  41402  eelTT1  41403  eel0T1  41405  nn0digval  45001  dignn0flhalf  45019  sinhpcosh  45253  reseccl  45266  recsccl  45267  recotcl  45268  onetansqsecsq  45274
  Copyright terms: Public domain W3C validator