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  4602  tfrlem9  6417  oaord1  6565  oaword2  6567  oawordeulem  6568  oa00  6573  omword1  6587  omword2  6588  omlimcl  6592  oeoelem  6612  nnaordex  6652  enp1i  7109  unfilem2  7138  dffi3  7200  unbnn3  7375  pwcdaen  7827  ackbij1b  7881  zorn2  8149  zornn0  8151  ttukey  8161  brdom7disj  8172  brdom6disj  8173  wunex2  8376  muladd11  8998  00id  9003  mul02  9006  negsubdi  9119  mulneg1  9232  ltaddpos  9280  addge01  9300  reccl  9447  recid  9454  recid2  9455  recdiv2  9489  divdiv23zi  9529  ltmul12a  9628  lemul12a  9630  mulgt1  9631  ltmulgt11  9632  gt0div  9638  ge0div  9639  lediv12a  9665  ledivp1  9674  ltdiv23i  9697  ledivp1i  9698  ltdivp1i  9699  infm3  9729  infmrcl  9749  nngt1ne1  9789  8th4div3  9951  gtndiv  10105  nn0ind  10124  fnn0ind  10127  supminf  10321  xrre2  10515  qsqueeze  10544  xmulpnf1  10610  xlemul1a  10624  xrub  10646  ioorebas  10761  expubnd  11178  le2sq2  11195  crreczi  11242  bernneq  11243  faclbnd5  11327  faclbnd6  11328  bccl  11350  hashbc  11407  ccatlid  11450  shftfval  11581  mulre  11622  sqrlem4  11747  sqrlem7  11750  sqreulem  11859  binom1p  12305  0.999...  12353  efsub  12396  efi4p  12433  sinadd  12460  cosadd  12461  cos2t  12474  cos2tsin  12475  sin01gt0  12486  cos01gt0  12487  absefib  12494  efieq1re  12495  demoivreALT  12497  rpnnen2lem4  12512  odd2np1  12603  divalglem0  12608  divalglem4  12611  divalglem9  12616  gcdcllem3  12708  gcdn0gt0  12717  gcdadd  12725  gcdmultiple  12745  algcvgblem  12763  algcvga  12765  isprm3  12783  coprm  12795  divgcdodd  12814  phibndlem  12854  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pythagtriplem4  12888  pythagtriplem11  12894  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem14  12897  infpn2  12976  1arith2  12991  vdwap0  13039  vdwap1  13040  ipolt  14278  gsumval2a  14475  mplsubrglem  16199  cnfldneg  16416  cnflddiv  16420  cnfldmulg  16422  cnfldexp  16423  thlleval  16614  iccordt  16960  divstgplem  17819  bl2ioo  18314  ioo2blex  18316  blssioo  18317  tgioo  18318  xrsblre  18333  iccntr  18342  icccmplem3  18345  reconnlem2  18348  opnreen  18352  iccpnfcnv  18458  cnllycmp  18470  pcoptcl  18535  ovolmge0  18852  ovolctb2  18867  ismbl2  18902  cmmbl  18908  nulmbl  18909  unmbl  18911  voliunlem1  18923  voliunlem2  18924  ioombl1  18935  opnmbllem  18972  mbfima  19003  i1fsub  19079  itg1sub  19080  ellimc3  19245  limcflf  19247  dvcnvre  19382  coe1termlem  19655  dgrsub  19669  dvnply2  19683  dvnply  19684  reeff1o  19839  sinperlem  19864  sincosq1eq  19896  resinf1o  19914  logeftb  19953  logge0  19975  logdivlti  19987  efopn  20021  logtayl2  20025  loglesqr  20114  logrec  20133  xrlimcnp  20279  ppinncl  20428  chtrpcl  20429  bposlem2  20540  bposlem8  20546  lgsdir2  20583  1lgs  20592  isgrpoi  20881  grpo2grp  20917  imsmetlem  21275  nmcvcn  21284  ipval2  21296  lnocoi  21351  nmlno0lem  21387  nmblolbii  21393  blometi  21397  blocnilem  21398  blocni  21399  ipasslem1  21425  ipasslem2  21426  ipasslem4  21428  ipasslem5  21429  ipasslem8  21431  ipblnfi  21450  ip2eqi  21451  ubthlem1  21465  htthlem  21513  h2hmetdval  21574  axhvcom-zf  21579  axhis1-zf  21590  axhis4-zf  21593  hvm1neg  21627  hvsub4  21632  hvsubass  21639  hvsubdistr2  21645  hv2times  21656  hvsubcan  21669  hvsubcan2  21670  his2sub  21687  norm-i  21724  normpyc  21741  hhip  21772  hhph  21773  norm1exi  21845  hhssabloi  21855  hhssnv  21857  hhshsslem2  21861  hhssmetdval  21871  shscli  21912  shunssi  21963  shsleji  21965  shsidmi  21979  spanunsni  22174  h1datomi  22176  spansncvi  22247  pjss2i  22275  pjssmii  22276  pjocini  22293  homulid2  22396  honegdi  22405  ho2times  22415  nmopge0  22507  nmopgt0  22508  nmfnge0  22523  lnopaddi  22567  lnopmuli  22568  lnopsubi  22570  hmopbdoptHIL  22584  nmbdoplbi  22620  nmcoplbi  22624  nmophmi  22627  lnopconi  22630  lnfnaddi  22639  lnfnsubi  22642  nmbdfnlbi  22645  nmcfnlbi  22648  lnfnconi  22651  imaelshi  22654  cnlnadjlem2  22664  cnlnadjlem7  22669  nmoptrii  22690  nmopcoi  22691  adjcoi  22696  nmopcoadji  22697  bracnlnval  22710  leopmul  22730  opsqrlem1  22736  opsqrlem6  22741  hmopidmpji  22748  sto2i  22833  strlem1  22846  atcveq0  22944  atcv0eq  22975  atomli  22978  atcvati  22982  atcvat3i  22992  cdjreui  23028  cdj1i  23029  xdiv0  23128  xdivpnfrp  23133  mhmhmeotmd  23315  blscon  23790  cnllyscon  23791  ghomgrpilem2  24008  ghomsn  24010  sinccvglem  24020  wfrlem12  24338  frrlem11  24364  nobndlem8  24424  brbtwn2  24605  colinearalglem4  24609  ax5seglem1  24628  ax5seglem2  24629  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  bpoly3  24865  fsumcube  24867  seqzp2  25458  altretop  25703  nolimf  25722  cnegvex2  25763  rnegvex2  25764  vtarsuelt  25998  opnrebl2  26339  fimaxOLD  26511  heiborlem7  26644  rrnequiv  26662  ismrer1  26665  mapco2  26894  mzpaddmpt  26922  mzpmulmpt  26923  zindbi  27134  frlmsslsp  27351  mpaaeu  27458  f1otrspeq  27493  redwlklem  28363  sgnp  28501  eel000cT  28783  eel0TT  28784  eel011  28787  eel012  28789  eel0121  28790  eel001  28793  cnaddcom  29783
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