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

Theorem syl3an2 1400
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 1283 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 34 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1275 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  syl3an2b  1403  syl3an2br  1406  syl3anl2  1415  odi  7704  omass  7705  nndi  7748  nnmass  7749  omabslem  7771  winainf  9554  divsubdir  10759  divdiv32  10771  ltdiv2  10947  peano2uz  11779  irrmul  11851  supxrunb1  12187  fzoshftral  12625  ltdifltdiv  12675  axdc4uzlem  12822  expdiv  12951  bcval5  13145  ccats1val1  13446  rediv  13915  imdiv  13922  absdiflt  14101  absdifle  14102  iseraltlem3  14458  retancl  14916  tanneg  14922  lcmgcdeq  15372  prmdvdsexpb  15475  dvdsprmpweqnn  15636  mulgaddcomlem  17610  mulginvcom  17612  pmtrfb  17931  lspssp  19036  mdetunilem7  20472  m2detleiblem3  20483  m2detleiblem4  20484  pmatcollpw  20634  pmatcollpwscmat  20644  chpmatply1  20685  chfacfscmulgsum  20713  chfacfpmmulcl  20714  chfacfpmmul0  20715  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmadurid  20720  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmidgsum2  20732  islp2  20997  fmfg  21800  fmufil  21810  flffbas  21846  lmflf  21856  uffcfflf  21890  blres  22283  ncvsge0  22999  caucfil  23127  cmetcusp1  23195  deg1mul3  23920  quotval  24092  cusgr3vnbpr  26388  clwwlkinwwlk  27003  nvsge0  27647  hvsubass  28029  hvsubdistr2  28035  hvsubcan  28059  his2sub  28077  chlub  28496  spanunsni  28566  homco1  28788  homulass  28789  cnlnadjlem2  29055  adjmul  29079  chirredlem2  29378  atmd2  29387  mdsymlem5  29394  climuzcnv  31691  f1ocan2fv  33652  isdrngo2  33887  atncvrN  34920  cvlatcvr1  34946  eluzrabdioph  37687  iocmbl  38115  rp-isfinite6  38181  dvconstbi  38850  eelT11  39249  eelT12  39251  eelTT1  39252  eel0T1  39254  nn0digval  42719  dignn0flhalf  42737  sinhpcosh  42809  reseccl  42822  recsccl  42823  recotcl  42824  onetansqsecsq  42830
  Copyright terms: Public domain W3C validator