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

Theorem mp3an3 1349
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an3.1  |-  ch
mp3an3.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an3  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mp3an3
StepHypRef Expression
1 mp3an3.1 . 2  |-  ch
2 mp3an3.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expia 1207 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 21 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mp3an13  1351  mp3an23  1352  mp3anl3  1356  opelxp  4884  ov  6430  ovmpt2a  6441  ovmpt2  6446  oaword1  7261  oneo  7290  oeoalem  7305  oeoelem  7307  nnaword1  7338  nnneo  7360  erov  7468  enrefg  7608  f1imaen  7638  mapxpen  7744  acnlem  8477  cdacomen  8609  infmap  8999  canthnumlem  9072  tskin  9183  tsksn  9184  tsk0  9187  gruxp  9231  gruina  9242  genpprecl  9425  addsrpr  9498  mulsrpr  9499  supsrlem  9534  mulid1  9639  00id  9807  mul02lem1  9808  ltneg  10113  leneg  10116  suble0  10127  div1  10298  nnaddcl  10631  nnmulcl  10632  nnge1  10635  nnsub  10648  2halves  10841  halfaddsub  10846  addltmul  10848  zleltp1  10987  nnaddm1cl  10993  zextlt  11010  eluzp1p1  11184  uzaddcl  11215  znq  11268  xrre  11464  xrre2  11465  fzshftral  11880  fraclt1  12035  expadd  12311  expmul  12314  expubnd  12330  sqmul  12335  bernneq  12395  faclbnd2  12473  faclbnd6  12481  hashgadd  12553  hashun2  12559  hashssdif  12584  hashfun  12604  ccatlcan  12813  ccatrcan  12814  shftval3  13118  sqrlem1  13285  caubnd2  13399  bpoly2  14088  bpoly3  14089  fsumcube  14091  efexp  14133  efival  14184  cos01gt0  14223  odd2np1  14343  divalglem5  14353  gcdmultiple  14489  sqgcd  14497  nn0seqcvgd  14500  phiprmpw  14693  eulerthlem2  14699  odzcllem  14706  omoe  14725  opeo  14726  pythagtriplem15  14742  pythagtriplem17  14744  pcelnn  14782  4sqlem3  14857  xpscfn  15416  fullfunc  15762  fthfunc  15763  prfcl  16039  curf1cl  16064  curfcl  16068  hofcl  16095  odinv  17150  lsmelvalix  17228  dprdval  17570  lsp0  18167  lss0v  18174  coe1scl  18815  zndvds0  19052  frlmlbs  19286  lindfres  19312  lmisfree  19331  ntrin  20007  lpsscls  20088  restperf  20131  txuni2  20511  txopn  20548  elqtop2  20647  xkocnv  20760  ptcmp  21004  xblpnfps  21341  xblpnf  21342  bl2in  21346  unirnblps  21365  unirnbl  21366  blpnfctr  21382  dscopn  21519  bcthlem4  22188  minveclem2  22261  minveclem4  22267  icombl  22394  i1fadd  22530  i1fmul  22531  dvn1  22757  dvexp3  22807  plyconst  23028  plyid  23031  sincosq1eq  23332  sinord  23348  cxpp1  23490  cxpsqrtlem  23512  cxpsqrt  23513  angneg  23597  dcubic  23637  issqf  23926  ppiub  23995  bposlem1  24075  bposlem2  24076  bposlem9  24083  axlowdimlem6  24823  axlowdimlem14  24831  axcontlem2  24841  wwlkn0s  25278  clwwlkn2  25348  rusgranumwlkb0  25526  gx0  25834  gx1  25835  gxm1  25841  gxnn0add  25847  gxnn0mul  25850  ipasslem1  26317  ipasslem2  26318  ipasslem11  26326  minvecolem2  26362  minvecolem3  26363  minvecolem4  26367  shsva  26808  h1datomi  27069  lnfnmuli  27532  leopsq  27617  nmopleid  27627  opsqrlem6  27633  pjnmopi  27636  hstle  27718  csmdsymi  27822  atcvatlem  27873  elsx  28855  dya2iocnrect  28942  cvmliftphtlem  29828  wlimeq12  30289  nofulllem4  30379  fvray  30693  fvline  30696  tailfb  30818  tan2h  31641  poimirlem32  31676  mblfinlem4  31684  mbfresfi  31691  mbfposadd  31692  dvtanlemOLD  31695  itg2addnc  31700  ftc1anclem5  31725  ftc1anclem8  31728  dvasin  31732  heiborlem7  31853  igenidl  32000  atlatmstc  32594  dihglblem2N  34571  eldioph4b  35363  diophren  35365  rmxp1  35486  rmyp1  35487  rmxm1  35488  rmym1  35489  wepwso  35607  pfx2  38343  dig0  39178  onetansqsecsq  39242  cotsqcscsq  39243  dpfrac1  39253
  Copyright terms: Public domain W3C validator