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

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

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2  |-  ph
2 mp3an1.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expb 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 651 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mp3an12  1267  mp3an1i  1270  mp3anl1  1271  mp3an  1277  onint  4586  tfrlem9  6401  oaord1  6549  oaword2  6551  oawordeulem  6552  oa00  6557  omword1  6571  omword2  6572  omlimcl  6576  oeoelem  6596  nnaordex  6636  enp1i  7093  unfilem2  7122  dffi3  7184  unbnn3  7359  pwcdaen  7811  ackbij1b  7865  zorn2  8133  zornn0  8135  ttukey  8145  brdom7disj  8156  brdom6disj  8157  wunex2  8360  muladd11  8982  00id  8987  mul02  8990  negsubdi  9103  mulneg1  9216  ltaddpos  9264  addge01  9284  reccl  9431  recid  9438  recid2  9439  recdiv2  9473  divdiv23zi  9513  ltmul12a  9612  lemul12a  9614  mulgt1  9615  ltmulgt11  9616  gt0div  9622  ge0div  9623  lediv12a  9649  ledivp1  9658  ltdiv23i  9681  ledivp1i  9682  ltdivp1i  9683  infm3  9713  infmrcl  9733  nngt1ne1  9773  8th4div3  9935  gtndiv  10089  nn0ind  10108  fnn0ind  10111  supminf  10305  xrre2  10499  qsqueeze  10528  xmulpnf1  10594  xlemul1a  10608  xrub  10630  ioorebas  10745  expubnd  11162  le2sq2  11179  crreczi  11226  bernneq  11227  faclbnd5  11311  faclbnd6  11312  bccl  11334  hashbc  11391  ccatlid  11434  shftfval  11565  mulre  11606  sqrlem4  11731  sqrlem7  11734  sqreulem  11843  binom1p  12289  0.999...  12337  efsub  12380  efi4p  12417  sinadd  12444  cosadd  12445  cos2t  12458  cos2tsin  12459  sin01gt0  12470  cos01gt0  12471  absefib  12478  efieq1re  12479  demoivreALT  12481  rpnnen2lem4  12496  odd2np1  12587  divalglem0  12592  divalglem4  12595  divalglem9  12600  gcdcllem3  12692  gcdn0gt0  12701  gcdadd  12709  gcdmultiple  12729  algcvgblem  12747  algcvga  12749  isprm3  12767  coprm  12779  divgcdodd  12798  phibndlem  12838  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pythagtriplem4  12872  pythagtriplem11  12878  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  infpn2  12960  1arith2  12975  vdwap0  13023  vdwap1  13024  ipolt  14262  gsumval2a  14459  mplsubrglem  16183  cnfldneg  16400  cnflddiv  16404  cnfldmulg  16406  cnfldexp  16407  thlleval  16598  iccordt  16944  divstgplem  17803  bl2ioo  18298  ioo2blex  18300  blssioo  18301  tgioo  18302  xrsblre  18317  iccntr  18326  icccmplem3  18329  reconnlem2  18332  opnreen  18336  iccpnfcnv  18442  cnllycmp  18454  pcoptcl  18519  ovolmge0  18836  ovolctb2  18851  ismbl2  18886  cmmbl  18892  nulmbl  18893  unmbl  18895  voliunlem1  18907  voliunlem2  18908  ioombl1  18919  opnmbllem  18956  mbfima  18987  i1fsub  19063  itg1sub  19064  ellimc3  19229  limcflf  19231  dvcnvre  19366  coe1termlem  19639  dgrsub  19653  dvnply2  19667  dvnply  19668  reeff1o  19823  sinperlem  19848  sincosq1eq  19880  resinf1o  19898  logeftb  19937  logge0  19959  logdivlti  19971  efopn  20005  logtayl2  20009  loglesqr  20098  logrec  20117  xrlimcnp  20263  ppinncl  20412  chtrpcl  20413  bposlem2  20524  bposlem8  20530  lgsdir2  20567  1lgs  20576  isgrpoi  20865  grpo2grp  20901  imsmetlem  21259  nmcvcn  21268  ipval2  21280  lnocoi  21335  nmlno0lem  21371  nmblolbii  21377  blometi  21381  blocnilem  21382  blocni  21383  ipasslem1  21409  ipasslem2  21410  ipasslem4  21412  ipasslem5  21413  ipasslem8  21415  ipblnfi  21434  ip2eqi  21435  ubthlem1  21449  htthlem  21497  h2hmetdval  21558  axhvcom-zf  21563  axhis1-zf  21574  axhis4-zf  21577  hvm1neg  21611  hvsub4  21616  hvsubass  21623  hvsubdistr2  21629  hv2times  21640  hvsubcan  21653  hvsubcan2  21654  his2sub  21671  norm-i  21708  normpyc  21725  hhip  21756  hhph  21757  norm1exi  21829  hhssabloi  21839  hhssnv  21841  hhshsslem2  21845  hhssmetdval  21855  shscli  21896  shunssi  21947  shsleji  21949  shsidmi  21963  spanunsni  22158  h1datomi  22160  spansncvi  22231  pjss2i  22259  pjssmii  22260  pjocini  22277  homulid2  22380  honegdi  22389  ho2times  22399  nmopge0  22491  nmopgt0  22492  nmfnge0  22507  lnopaddi  22551  lnopmuli  22552  lnopsubi  22554  hmopbdoptHIL  22568  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  lnopconi  22614  lnfnaddi  22623  lnfnsubi  22626  nmbdfnlbi  22629  nmcfnlbi  22632  lnfnconi  22635  imaelshi  22638  cnlnadjlem2  22648  cnlnadjlem7  22653  nmoptrii  22674  nmopcoi  22675  adjcoi  22680  nmopcoadji  22681  bracnlnval  22694  leopmul  22714  opsqrlem1  22720  opsqrlem6  22725  hmopidmpji  22732  sto2i  22817  strlem1  22830  atcveq0  22928  atcv0eq  22959  atomli  22962  atcvati  22966  atcvat3i  22976  cdjreui  23012  cdj1i  23013  blscon  23186  cnllyscon  23187  ghomgrpilem2  23404  ghomsn  23406  sinccvglem  23416  wfrlem12  23678  frrlem11  23704  nobndlem8  23764  brbtwn2  23944  colinearalglem4  23948  ax5seglem1  23967  ax5seglem2  23968  axcontlem2  24004  axcontlem4  24006  axcontlem7  24009  bpoly3  24204  fsumcube  24206  seqzp2  24767  altretop  25012  nolimf  25031  cnegvex2  25072  rnegvex2  25073  vtarsuelt  25307  opnrebl2  25648  fimaxOLD  25820  heiborlem7  25953  rrnequiv  25971  ismrer1  25974  mapco2  26203  mzpaddmpt  26231  mzpmulmpt  26232  zindbi  26443  frlmsslsp  26660  mpaaeu  26767  f1otrspeq  26802  sgnp  27609  eel000cT  27851  eel0TT  27852  eel011  27855  eel012  27857  eel001  27860  cnaddcom  28534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator