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

Theorem mp3an1 1347
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 1206 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 674 1  |-  ( ( ps  /\  ch )  ->  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:  mp3an12  1350  mp3an1i  1353  mp3anl1  1354  mp3an  1360  onint  6636  wfrlem12  7055  wfrlem17  7060  tfrlem9  7111  oaord1  7260  oaword2  7262  oawordeulem  7263  oa00  7268  omword1  7282  omword2  7283  omlimcl  7287  oeoelem  7307  nnaordex  7347  enp1i  7812  unfilem2  7842  dffi3  7951  unbnn3  8163  pwcdaen  8613  ackbij1b  8667  zorn2  8934  zornn0  8936  ttukey  8946  brdom7disj  8957  brdom6disj  8958  wunex2  9162  muladd11  9802  00id  9807  mul02  9810  negsubdi  9929  mulneg1  10054  ltaddpos  10103  addge01  10123  reccl  10276  recid  10283  recid2  10284  recdiv2  10319  divdiv23zi  10359  ltmul12a  10460  lemul12a  10462  mulgt1  10463  ltmulgt11  10464  gt0div  10470  ge0div  10471  lediv12a  10499  ledivp1  10508  ltdiv23i  10531  ledivp1i  10532  ltdivp1i  10533  infm3  10568  infmrclOLD  10593  nngt1ne1  10636  8th4div3  10833  gtndiv  11013  nn0ind  11030  fnn0ind  11034  supminf  11250  supminfOLD  11251  xrre2  11465  qsqueeze  11494  xmulpnf1  11560  xlemul1a  11574  xrub  11597  ioorebas  11736  elfz0ubfz0  11892  expubnd  12330  le2sq2  12347  crreczi  12394  bernneq  12395  faclbnd5  12480  faclbnd6  12481  bccl  12504  hashbc  12611  ccatlid  12717  shftfval  13112  sgnp  13132  mulre  13163  sqrlem4  13288  sqrlem7  13291  sqreulem  13401  binom1p  13867  0.999...  13915  fallrisefac  14056  bpoly3  14089  fsumcube  14091  efsub  14132  efi4p  14169  sinadd  14196  cosadd  14197  cos2t  14210  cos2tsin  14211  sin01gt0  14222  cos01gt0  14223  absefib  14230  efieq1re  14231  demoivreALT  14233  rpnnen2lem4  14248  odd2np1  14343  divalglem0  14349  divalglem4  14352  divalglem9  14357  gcdcllem3  14449  gcdn0gt0  14460  gcdadd  14468  gcdmultiple  14489  algcvgblem  14507  algcvga  14509  isprm3  14604  divgcdodd  14624  coprm  14628  phibndlem  14687  opoe  14724  omoe  14725  opeo  14726  omeo  14727  pythagtriplem4  14732  pythagtriplem11  14738  pythagtriplem12  14739  pythagtriplem13  14740  pythagtriplem14  14741  infpn2  14820  1arith2  14835  vdwap0  14889  vdwap1  14890  ipolt  16356  gsumval2a  16473  f1otrspeq  17039  mplsubrglem  18598  evls1rhm  18846  cnfldneg  18929  cnflddiv  18933  cnfldmulg  18935  cnfldexp  18936  zringmulg  18981  remulg  19106  resubgval  19108  thlleval  19192  frlmsslsp  19285  neiptoptop  20078  iccordt  20161  qustgplem  21066  bl2ioo  21721  ioo2blex  21723  blssioo  21724  tgioo  21725  xrsblre  21740  iccntr  21750  icccmplem3  21753  reconnlem2  21756  opnreen  21760  iccpnfcnv  21868  cnllycmp  21880  pcoptcl  21945  ovolmge0  22308  ovolctb2  22323  ismbl2  22358  cmmbl  22365  nulmbl  22366  unmbl  22368  voliunlem1  22380  voliunlem2  22381  ioombl1  22392  opnmbllem  22436  mbfima  22465  i1fsub  22543  itg1sub  22544  ellimc3  22711  limcflf  22713  dvcnvre  22848  coe1termlem  23080  dgrsub  23094  dvnply2  23108  dvnply  23109  reeff1o  23267  sinperlem  23300  sincosq1eq  23332  resinf1o  23350  logeftb  23398  logge0  23419  logdivlti  23434  efopn  23468  logtayl2  23472  loglesqrt  23563  logrec  23565  xrlimcnp  23759  ppinncl  23964  chtrpcl  23965  bposlem2  24076  bposlem8  24082  lgsdir2  24119  1lgs  24128  brbtwn2  24781  colinearalglem4  24785  ax5seglem1  24804  ax5seglem2  24805  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  iswlkg  25097  redwlklem  25180  0vgrargra  25510  isgrpoi  25771  grpo2grp  25807  imsmetlem  26167  nmcvcn  26176  ipval2  26188  lnocoi  26243  nmlno0lem  26279  nmblolbii  26285  blometi  26289  blocnilem  26290  blocni  26291  ipasslem1  26317  ipasslem2  26318  ipasslem4  26320  ipasslem5  26321  ipasslem8  26323  ipblnfi  26342  ip2eqi  26343  ubthlem1  26357  htthlem  26405  h2hmetdval  26466  axhvcom-zf  26471  axhis1-zf  26482  axhis4-zf  26485  hvm1neg  26520  hvsub4  26525  hvsubass  26532  hvsubdistr2  26538  hv2times  26549  hvsubcan  26562  hvsubcan2  26563  his2sub  26580  norm-i  26617  normpyc  26634  hhip  26665  hhph  26666  norm1exi  26738  hhssabloi  26748  hhssnv  26750  hhshsslem2  26754  hhssmetdval  26764  shscli  26805  shunssi  26856  shsleji  26858  shsidmi  26872  spanunsni  27067  h1datomi  27069  spansncvi  27140  pjss2i  27168  pjssmii  27169  pjocini  27186  homulid2  27288  honegdi  27297  ho2times  27307  nmopge0  27399  nmopgt0  27400  nmfnge0  27415  lnopaddi  27459  lnopmuli  27460  lnopsubi  27462  hmopbdoptHIL  27476  nmbdoplbi  27512  nmcoplbi  27516  nmophmi  27519  lnopconi  27522  lnfnaddi  27531  lnfnsubi  27534  nmbdfnlbi  27537  nmcfnlbi  27540  lnfnconi  27543  imaelshi  27546  cnlnadjlem2  27556  cnlnadjlem7  27561  nmoptrii  27582  nmopcoi  27583  adjcoi  27588  nmopcoadji  27589  bracnlnval  27602  leopmul  27622  opsqrlem1  27628  opsqrlem6  27633  hmopidmpji  27640  sto2i  27725  strlem1  27738  atcveq0  27836  atcv0eq  27867  atomli  27870  atcvati  27874  atcvat3i  27884  cdjreui  27920  cdj1i  27921  xdiv0  28236  xdivpnfrp  28240  mhmhmeotmd  28572  rezh  28614  qqhucn  28635  blscon  29755  cnllyscon  29756  ghomgrpilem2  30092  ghomsn  30094  sinccvglem  30104  frrlem11  30313  nobndlem8  30373  opnrebl2  30762  ptrecube  31644  poimirlem6  31650  poimirlem7  31651  poimirlem29  31673  poimirlem30  31674  opnmbllem0  31680  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  voliunnfl  31688  ftc1anclem5  31725  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  heiborlem7  31853  rrnequiv  31871  ismrer1  31874  cnaddcom  32247  mapco2  35266  mzpaddmpt  35292  mzpmulmpt  35293  zindbi  35500  mpaaeu  35715  eel000cT  36722  eel0TT  36723  eel011  36726  eel012  36728  zringsubgval  38956  aacllem  39310
  Copyright terms: Public domain W3C validator