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

Theorem syl3an2 1351
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an2.1 (𝜑𝜒)
syl3an2.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an2 ((𝜓𝜑𝜃) → 𝜏)

Proof of Theorem syl3an2
StepHypRef Expression
1 syl3an2.1 . . 3 (𝜑𝜒)
2 syl3an2.2 . . . 4 ((𝜓𝜒𝜃) → 𝜏)
323exp 1255 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 33 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1248 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  syl3an2b  1354  syl3an2br  1357  syl3anl2  1366  odi  7523  omass  7524  nndi  7567  nnmass  7568  omabslem  7590  winainf  9372  divsubdir  10570  divdiv32  10582  ltdiv2  10758  peano2uz  11573  irrmul  11645  supxrunb1  11977  fzoshftral  12402  ltdifltdiv  12452  axdc4uzlem  12599  expdiv  12728  bcval5  12922  ccats1val1  13201  rediv  13665  imdiv  13672  absdiflt  13851  absdifle  13852  iseraltlem3  14208  retancl  14657  tanneg  14663  lcmgcdeq  15109  prmdvdsexpb  15212  dvdsprmpweqnn  15373  mulgaddcomlem  17332  mulginvcom  17334  pmtrfb  17654  lspssp  18755  mdetunilem7  20185  m2detleiblem3  20196  m2detleiblem4  20197  pmatcollpw  20347  pmatcollpwscmat  20357  chpmatply1  20398  chfacfscmulgsum  20426  chfacfpmmulcl  20427  chfacfpmmul0  20428  chfacfpmmulgsum  20430  chfacfpmmulgsum2  20431  cayhamlem1  20432  cpmadurid  20433  cpmadugsumlemC  20441  cpmadugsumlemF  20442  cpmadugsumfi  20443  cpmidgsum2  20445  islp2  20701  fmfg  21505  fmufil  21515  flffbas  21551  lmflf  21561  uffcfflf  21595  blres  21987  ncvsge0  22687  caucfil  22807  cmetcusp1  22874  deg1mul3  23596  quotval  23768  cusgra3vnbpr  25760  nvsge0  26696  hvsubass  27091  hvsubdistr2  27097  hvsubcan  27121  his2sub  27139  chlub  27558  spanunsni  27628  homco1  27850  homulass  27851  cnlnadjlem2  28117  adjmul  28141  chirredlem2  28440  atmd2  28449  mdsymlem5  28456  climuzcnv  30625  f1ocan2fv  32488  isdrngo2  32723  atncvrN  33416  cvlatcvr1  33442  eluzrabdioph  36184  iocmbl  36613  rp-isfinite6  36679  dvconstbi  37351  eelT11  37749  eelT12  37751  eelTT1  37752  eel0T1  37754  cusgr3vnbpr  40653  nn0digval  42187  dignn0flhalf  42205  sinhpcosh  42236  reseccl  42249  recsccl  42250  recotcl  42251  onetansqsecsq  42257
  Copyright terms: Public domain W3C validator