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

Theorem mp3an1 1310
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 1196 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 670 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 371  df-3an 974
This theorem is referenced by:  mp3an12  1313  mp3an1i  1316  mp3anl1  1317  mp3an  1323  onint  6611  tfrlem9  7052  oaord1  7198  oaword2  7200  oawordeulem  7201  oa00  7206  omword1  7220  omword2  7221  omlimcl  7225  oeoelem  7245  nnaordex  7285  enp1i  7753  unfilem2  7783  dffi3  7889  unbnn3  8073  pwcdaen  8563  ackbij1b  8617  zorn2  8884  zornn0  8886  ttukey  8896  brdom7disj  8907  brdom6disj  8908  wunex2  9114  muladd11  9748  00id  9753  mul02  9756  negsubdi  9875  mulneg1  9994  ltaddpos  10043  addge01  10063  reccl  10215  recid  10222  recid2  10223  recdiv2  10258  divdiv23zi  10298  ltmul12a  10399  lemul12a  10401  mulgt1  10402  ltmulgt11  10403  gt0div  10409  ge0div  10410  lediv12a  10439  ledivp1  10448  ltdiv23i  10471  ledivp1i  10472  ltdivp1i  10473  infm3  10503  infmrcl  10523  nngt1ne1  10564  8th4div3  10760  gtndiv  10941  nn0ind  10960  fnn0ind  10963  supminf  11173  xrre2  11375  qsqueeze  11404  xmulpnf1  11470  xlemul1a  11484  xrub  11507  ioorebas  11630  elfz0ubfz0  11781  expubnd  12200  le2sq2  12217  crreczi  12265  bernneq  12266  faclbnd5  12350  faclbnd6  12351  bccl  12374  hashbc  12476  ccatlid  12577  shftfval  12877  sgnp  12897  mulre  12928  sqrlem4  13053  sqrlem7  13056  sqreulem  13166  binom1p  13617  0.999...  13664  efsub  13707  efi4p  13744  sinadd  13771  cosadd  13772  cos2t  13785  cos2tsin  13786  sin01gt0  13797  cos01gt0  13798  absefib  13805  efieq1re  13806  demoivreALT  13808  rpnnen2lem4  13823  odd2np1  13918  divalglem0  13923  divalglem4  13926  divalglem9  13931  gcdcllem3  14023  gcdn0gt0  14032  gcdadd  14040  gcdmultiple  14060  algcvgblem  14078  algcvga  14080  isprm3  14098  coprm  14113  divgcdodd  14132  phibndlem  14172  opoe  14207  omoe  14208  opeo  14209  omeo  14210  pythagtriplem4  14215  pythagtriplem11  14221  pythagtriplem12  14222  pythagtriplem13  14223  pythagtriplem14  14224  infpn2  14303  1arith2  14318  vdwap0  14366  vdwap1  14367  ipolt  15658  gsumval2a  15775  f1otrspeq  16341  mplsubrglem  17968  mplsubrglemOLD  17969  evls1rhm  18227  cnfldneg  18312  cnflddiv  18316  cnfldmulg  18318  cnfldexp  18319  zringmulg  18364  zrngmulg  18370  remulg  18510  resubgval  18512  thlleval  18596  frlmsslsp  18696  frlmsslspOLD  18697  neiptoptop  19498  iccordt  19581  qustgplem  20485  bl2ioo  21163  ioo2blex  21165  blssioo  21166  tgioo  21167  xrsblre  21182  iccntr  21192  icccmplem3  21195  reconnlem2  21198  opnreen  21202  iccpnfcnv  21310  cnllycmp  21322  pcoptcl  21387  ovolmge0  21754  ovolctb2  21769  ismbl2  21804  cmmbl  21811  nulmbl  21812  unmbl  21814  voliunlem1  21826  voliunlem2  21827  ioombl1  21838  opnmbllem  21876  mbfima  21905  i1fsub  21981  itg1sub  21982  ellimc3  22149  limcflf  22151  dvcnvre  22286  coe1termlem  22520  dgrsub  22534  dvnply2  22548  dvnply  22549  reeff1o  22707  sinperlem  22738  sincosq1eq  22770  resinf1o  22788  logeftb  22833  logge0  22855  logdivlti  22870  efopn  22904  logtayl2  22908  loglesqrt  22997  logrec  23016  xrlimcnp  23163  ppinncl  23313  chtrpcl  23314  bposlem2  23425  bposlem8  23431  lgsdir2  23468  1lgs  23477  brbtwn2  24073  colinearalglem4  24077  ax5seglem1  24096  ax5seglem2  24097  axcontlem2  24133  axcontlem4  24135  axcontlem7  24138  iswlkg  24389  redwlklem  24472  0vgrargra  24802  isgrpoi  25065  grpo2grp  25101  imsmetlem  25461  nmcvcn  25470  ipval2  25482  lnocoi  25537  nmlno0lem  25573  nmblolbii  25579  blometi  25583  blocnilem  25584  blocni  25585  ipasslem1  25611  ipasslem2  25612  ipasslem4  25614  ipasslem5  25615  ipasslem8  25617  ipblnfi  25636  ip2eqi  25637  ubthlem1  25651  htthlem  25699  h2hmetdval  25760  axhvcom-zf  25765  axhis1-zf  25776  axhis4-zf  25779  hvm1neg  25814  hvsub4  25819  hvsubass  25826  hvsubdistr2  25832  hv2times  25843  hvsubcan  25856  hvsubcan2  25857  his2sub  25874  norm-i  25911  normpyc  25928  hhip  25959  hhph  25960  norm1exi  26033  hhssabloi  26043  hhssnv  26045  hhshsslem2  26049  hhssmetdval  26059  shscli  26100  shunssi  26151  shsleji  26153  shsidmi  26167  spanunsni  26362  h1datomi  26364  spansncvi  26435  pjss2i  26463  pjssmii  26464  pjocini  26481  homulid2  26584  honegdi  26593  ho2times  26603  nmopge0  26695  nmopgt0  26696  nmfnge0  26711  lnopaddi  26755  lnopmuli  26756  lnopsubi  26758  hmopbdoptHIL  26772  nmbdoplbi  26808  nmcoplbi  26812  nmophmi  26815  lnopconi  26818  lnfnaddi  26827  lnfnsubi  26830  nmbdfnlbi  26833  nmcfnlbi  26836  lnfnconi  26839  imaelshi  26842  cnlnadjlem2  26852  cnlnadjlem7  26857  nmoptrii  26878  nmopcoi  26879  adjcoi  26884  nmopcoadji  26885  bracnlnval  26898  leopmul  26918  opsqrlem1  26924  opsqrlem6  26929  hmopidmpji  26936  sto2i  27021  strlem1  27034  atcveq0  27132  atcv0eq  27163  atomli  27166  atcvati  27170  atcvat3i  27180  cdjreui  27216  cdj1i  27217  xdiv0  27491  xdivpnfrp  27495  mhmhmeotmd  27775  rezh  27818  qqhucn  27839  blscon  28555  cnllyscon  28556  ghomgrpilem2  28892  ghomsn  28894  sinccvglem  28904  fallrisefac  29115  wfrlem12  29322  frrlem11  29367  nobndlem8  29427  bpoly3  29788  fsumcube  29790  opnmbllem0  30018  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  voliunnfl  30026  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  opnrebl2  30107  heiborlem7  30281  rrnequiv  30299  ismrer1  30302  mapco2  30615  mzpaddmpt  30641  mzpmulmpt  30642  zindbi  30850  mpaaeu  31068  zringsubgval  32705  eel000cT  33199  eel0TT  33200  eel011  33203  eel012  33205  cnaddcom  34399
  Copyright terms: Public domain W3C validator