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

Theorem mp3an1 1309
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 1195 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 668 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  mp3an12  1312  mp3an1i  1315  mp3anl1  1316  mp3an  1322  onint  6603  tfrlem9  7046  oaord1  7192  oaword2  7194  oawordeulem  7195  oa00  7200  omword1  7214  omword2  7215  omlimcl  7219  oeoelem  7239  nnaordex  7279  enp1i  7747  unfilem2  7777  dffi3  7883  unbnn3  8066  pwcdaen  8556  ackbij1b  8610  zorn2  8877  zornn0  8879  ttukey  8889  brdom7disj  8900  brdom6disj  8901  wunex2  9105  muladd11  9739  00id  9744  mul02  9747  negsubdi  9866  mulneg1  9989  ltaddpos  10038  addge01  10058  reccl  10210  recid  10217  recid2  10218  recdiv2  10253  divdiv23zi  10293  ltmul12a  10394  lemul12a  10396  mulgt1  10397  ltmulgt11  10398  gt0div  10404  ge0div  10405  lediv12a  10433  ledivp1  10442  ltdiv23i  10465  ledivp1i  10466  ltdivp1i  10467  infm3  10497  infmrcl  10517  nngt1ne1  10558  8th4div3  10755  gtndiv  10936  nn0ind  10955  fnn0ind  10959  supminf  11170  xrre2  11374  qsqueeze  11403  xmulpnf1  11469  xlemul1a  11483  xrub  11506  ioorebas  11629  elfz0ubfz0  11782  expubnd  12208  le2sq2  12225  crreczi  12273  bernneq  12274  faclbnd5  12358  faclbnd6  12359  bccl  12382  hashbc  12486  ccatlid  12592  shftfval  12985  sgnp  13005  mulre  13036  sqrlem4  13161  sqrlem7  13164  sqreulem  13274  binom1p  13725  0.999...  13772  efsub  13917  efi4p  13954  sinadd  13981  cosadd  13982  cos2t  13995  cos2tsin  13996  sin01gt0  14007  cos01gt0  14008  absefib  14015  efieq1re  14016  demoivreALT  14018  rpnnen2lem4  14035  odd2np1  14130  divalglem0  14135  divalglem4  14138  divalglem9  14143  gcdcllem3  14235  gcdn0gt0  14244  gcdadd  14252  gcdmultiple  14272  algcvgblem  14290  algcvga  14292  isprm3  14310  coprm  14325  divgcdodd  14344  phibndlem  14384  opoe  14419  omoe  14420  opeo  14421  omeo  14422  pythagtriplem4  14427  pythagtriplem11  14433  pythagtriplem12  14434  pythagtriplem13  14435  pythagtriplem14  14436  infpn2  14515  1arith2  14530  vdwap0  14578  vdwap1  14579  ipolt  15988  gsumval2a  16105  f1otrspeq  16671  mplsubrglem  18295  mplsubrglemOLD  18296  evls1rhm  18554  cnfldneg  18639  cnflddiv  18643  cnfldmulg  18645  cnfldexp  18646  zringmulg  18691  remulg  18816  resubgval  18818  thlleval  18902  frlmsslsp  18998  neiptoptop  19799  iccordt  19882  qustgplem  20785  bl2ioo  21463  ioo2blex  21465  blssioo  21466  tgioo  21467  xrsblre  21482  iccntr  21492  icccmplem3  21495  reconnlem2  21498  opnreen  21502  iccpnfcnv  21610  cnllycmp  21622  pcoptcl  21687  ovolmge0  22054  ovolctb2  22069  ismbl2  22104  cmmbl  22111  nulmbl  22112  unmbl  22114  voliunlem1  22126  voliunlem2  22127  ioombl1  22138  opnmbllem  22176  mbfima  22205  i1fsub  22281  itg1sub  22282  ellimc3  22449  limcflf  22451  dvcnvre  22586  coe1termlem  22821  dgrsub  22835  dvnply2  22849  dvnply  22850  reeff1o  23008  sinperlem  23039  sincosq1eq  23071  resinf1o  23089  logeftb  23137  logge0  23158  logdivlti  23173  efopn  23207  logtayl2  23211  loglesqrt  23300  logrec  23302  xrlimcnp  23496  ppinncl  23646  chtrpcl  23647  bposlem2  23758  bposlem8  23764  lgsdir2  23801  1lgs  23810  brbtwn2  24410  colinearalglem4  24414  ax5seglem1  24433  ax5seglem2  24434  axcontlem2  24470  axcontlem4  24472  axcontlem7  24475  iswlkg  24726  redwlklem  24809  0vgrargra  25139  isgrpoi  25398  grpo2grp  25434  imsmetlem  25794  nmcvcn  25803  ipval2  25815  lnocoi  25870  nmlno0lem  25906  nmblolbii  25912  blometi  25916  blocnilem  25917  blocni  25918  ipasslem1  25944  ipasslem2  25945  ipasslem4  25947  ipasslem5  25948  ipasslem8  25950  ipblnfi  25969  ip2eqi  25970  ubthlem1  25984  htthlem  26032  h2hmetdval  26093  axhvcom-zf  26098  axhis1-zf  26109  axhis4-zf  26112  hvm1neg  26147  hvsub4  26152  hvsubass  26159  hvsubdistr2  26165  hv2times  26176  hvsubcan  26189  hvsubcan2  26190  his2sub  26207  norm-i  26244  normpyc  26261  hhip  26292  hhph  26293  norm1exi  26366  hhssabloi  26376  hhssnv  26378  hhshsslem2  26382  hhssmetdval  26392  shscli  26433  shunssi  26484  shsleji  26486  shsidmi  26500  spanunsni  26695  h1datomi  26697  spansncvi  26768  pjss2i  26796  pjssmii  26797  pjocini  26814  homulid2  26917  honegdi  26926  ho2times  26936  nmopge0  27028  nmopgt0  27029  nmfnge0  27044  lnopaddi  27088  lnopmuli  27089  lnopsubi  27091  hmopbdoptHIL  27105  nmbdoplbi  27141  nmcoplbi  27145  nmophmi  27148  lnopconi  27151  lnfnaddi  27160  lnfnsubi  27163  nmbdfnlbi  27166  nmcfnlbi  27169  lnfnconi  27172  imaelshi  27175  cnlnadjlem2  27185  cnlnadjlem7  27190  nmoptrii  27211  nmopcoi  27212  adjcoi  27217  nmopcoadji  27218  bracnlnval  27231  leopmul  27251  opsqrlem1  27257  opsqrlem6  27262  hmopidmpji  27269  sto2i  27354  strlem1  27367  atcveq0  27465  atcv0eq  27496  atomli  27499  atcvati  27503  atcvat3i  27513  cdjreui  27549  cdj1i  27550  xdiv0  27859  xdivpnfrp  27863  mhmhmeotmd  28144  rezh  28186  qqhucn  28207  blscon  28953  cnllyscon  28954  ghomgrpilem2  29290  ghomsn  29292  sinccvglem  29302  fallrisefac  29388  wfrlem12  29594  frrlem11  29639  nobndlem8  29699  bpoly3  30048  fsumcube  30050  opnmbllem0  30290  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  voliunnfl  30298  ftc1anclem5  30334  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  opnrebl2  30379  heiborlem7  30553  rrnequiv  30571  ismrer1  30574  mapco2  30887  mzpaddmpt  30913  mzpmulmpt  30914  zindbi  31121  mpaaeu  31340  zringsubgval  33249  aacllem  33604  eel000cT  33885  eel0TT  33886  eel011  33889  eel012  33891  cnaddcom  35094
  Copyright terms: Public domain W3C validator