MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an3 Structured version   Unicode version

Theorem syl3an3 1261
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1  |-  ( ph  ->  th )
syl3an3.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an3  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3  |-  ( ph  ->  th )
2 syl3an3.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1193 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 68 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1188 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  syl3an3b  1264  syl3an3br  1267  vtoclgft  3154  disji  4427  ovmpt2x  6404  ovmpt2ga  6405  unbnn2  7769  axdc3lem4  8824  axdclem2  8891  gruiin  9177  gruen  9179  divass  10221  ltmul2  10389  xleadd1  11450  xltadd2  11452  xlemul1  11485  xltmul2  11488  elfzo  11806  modcyc2  12014  faclbnd5  12358  relexprel  12954  subcn2  13499  mulcn2  13500  ndvdsp1  14151  gcddiv  14271  lubel  15951  gsumccatsn  16210  oddvdsi  16771  odcong  16772  odeq  16773  efgsp1  16954  lspsnss  17831  lindsmm2  19031  mulmarep1el  19241  mdetunilem4  19284  iuncld  19713  neips  19781  opnneip  19787  comppfsc  20199  hmeof1o2  20430  ordthmeo  20469  ufinffr  20596  elfm3  20617  utop3cls  20920  blcntrps  21081  blcntr  21082  neibl  21170  blnei  21171  metss  21177  stdbdmetval  21183  prdsms  21200  blval2  21244  lmmbr  21863  lmmbr2  21864  iscau2  21882  bcthlem1  21929  bcthlem3  21931  bcthlem4  21932  dvn2bss  22499  dvfsumrlim  22598  dvfsumrlim2  22599  cxpexpz  23216  cxpsub  23231  relogbzexp  23315  wlkcompim  24728  wwlknext  24926  wwlkextproplem3  24945  clwlkcompim  24966  clwwlkel  24995  clwwlkf  24996  numclwlk1lem2f1  25296  gxpval  25459  gxnn0neg  25463  gxnn0suc  25464  gxcl  25465  gxneg  25466  gxcom  25469  gxinv  25470  gxsuc  25472  gxnn0add  25474  gxadd  25475  gxsub  25476  gxnn0mul  25477  gxmul  25478  hvaddsub12  26153  hvaddsubass  26156  hvsubdistr1  26164  hvsubcan  26189  hhssnv  26378  spanunsni  26695  homco1  26918  homulass  26919  hoadddir  26921  hosubdi  26925  hoaddsubass  26932  hosubsub4  26935  lnopmi  27117  adjlnop  27203  mdsymlem5  27524  disjif  27649  disjif2  27652  ind0  28249  sigaclfu  28349  wfrlem14  29596  ftc1anclem6  30335  clsint2  30387  isbnd2  30519  blbnd  30523  isdrngo2  30601  jm2.22  31176  jm2.23  31177  lcmneg  31450  dvconstbi  31480  rmfsupp  33221  mndpfsupp  33223  scmfsupp  33225  dignn0flhalflem2  33491  eelT11  33890  eelT12  33894  eelTT1  33896  eelT01  33897  eel0T1  33898  bnj544  34353  bnj561  34362  bnj562  34363  bnj594  34371  atnem0  35440  hlrelat5N  35522  ltrnel  36260  ltrnat  36261  ltrncnvat  36262
  Copyright terms: Public domain W3C validator