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

Theorem mp3an1 1311
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 1197 . 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 973
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 975
This theorem is referenced by:  mp3an12  1314  mp3an1i  1317  mp3anl1  1318  mp3an  1324  onint  6608  tfrlem9  7051  oaord1  7197  oaword2  7199  oawordeulem  7200  oa00  7205  omword1  7219  omword2  7220  omlimcl  7224  oeoelem  7244  nnaordex  7284  enp1i  7751  unfilem2  7781  dffi3  7887  unbnn3  8071  pwcdaen  8561  ackbij1b  8615  zorn2  8882  zornn0  8884  ttukey  8894  brdom7disj  8905  brdom6disj  8906  wunex2  9112  muladd11  9745  00id  9750  mul02  9753  negsubdi  9871  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  10434  ledivp1  10443  ltdiv23i  10466  ledivp1i  10467  ltdivp1i  10468  infm3  10498  infmrcl  10518  nngt1ne1  10559  8th4div3  10755  gtndiv  10934  nn0ind  10953  fnn0ind  10956  supminf  11165  xrre2  11367  qsqueeze  11396  xmulpnf1  11462  xlemul1a  11476  xrub  11499  ioorebas  11622  elfz0ubfz0  11772  expubnd  12190  le2sq2  12207  crreczi  12255  bernneq  12256  faclbnd5  12340  faclbnd6  12341  bccl  12364  hashbc  12464  ccatlid  12564  shftfval  12862  sgnp  12882  mulre  12913  sqrlem4  13038  sqrlem7  13041  sqreulem  13151  binom1p  13602  0.999...  13649  efsub  13692  efi4p  13729  sinadd  13756  cosadd  13757  cos2t  13770  cos2tsin  13771  sin01gt0  13782  cos01gt0  13783  absefib  13790  efieq1re  13791  demoivreALT  13793  rpnnen2lem4  13808  odd2np1  13901  divalglem0  13906  divalglem4  13909  divalglem9  13914  gcdcllem3  14006  gcdn0gt0  14015  gcdadd  14023  gcdmultiple  14043  algcvgblem  14061  algcvga  14063  isprm3  14081  coprm  14096  divgcdodd  14115  phibndlem  14155  opoe  14190  omoe  14191  opeo  14192  omeo  14193  pythagtriplem4  14198  pythagtriplem11  14204  pythagtriplem12  14205  pythagtriplem13  14206  pythagtriplem14  14207  infpn2  14286  1arith2  14301  vdwap0  14349  vdwap1  14350  ipolt  15642  gsumval2a  15825  f1otrspeq  16268  mplsubrglem  17871  mplsubrglemOLD  17872  evls1rhm  18130  cnfldneg  18215  cnflddiv  18219  cnfldmulg  18221  cnfldexp  18222  zringmulg  18264  zrngmulg  18270  remulg  18410  resubgval  18412  thlleval  18496  frlmsslsp  18596  frlmsslspOLD  18597  neiptoptop  19398  iccordt  19481  divstgplem  20354  bl2ioo  21032  ioo2blex  21034  blssioo  21035  tgioo  21036  xrsblre  21051  iccntr  21061  icccmplem3  21064  reconnlem2  21067  opnreen  21071  iccpnfcnv  21179  cnllycmp  21191  pcoptcl  21256  ovolmge0  21623  ovolctb2  21638  ismbl2  21673  cmmbl  21680  nulmbl  21681  unmbl  21683  voliunlem1  21695  voliunlem2  21696  ioombl1  21707  opnmbllem  21745  mbfima  21774  i1fsub  21850  itg1sub  21851  ellimc3  22018  limcflf  22020  dvcnvre  22155  coe1termlem  22389  dgrsub  22403  dvnply2  22417  dvnply  22418  reeff1o  22576  sinperlem  22606  sincosq1eq  22638  resinf1o  22656  logeftb  22696  logge0  22718  logdivlti  22733  efopn  22767  logtayl2  22771  loglesqrt  22860  logrec  22879  xrlimcnp  23026  ppinncl  23176  chtrpcl  23177  bposlem2  23288  bposlem8  23294  lgsdir2  23331  1lgs  23340  brbtwn2  23884  colinearalglem4  23888  ax5seglem1  23907  ax5seglem2  23908  axcontlem2  23944  axcontlem4  23946  axcontlem7  23949  iswlkg  24200  redwlklem  24283  0vgrargra  24613  isgrpoi  24876  grpo2grp  24912  imsmetlem  25272  nmcvcn  25281  ipval2  25293  lnocoi  25348  nmlno0lem  25384  nmblolbii  25390  blometi  25394  blocnilem  25395  blocni  25396  ipasslem1  25422  ipasslem2  25423  ipasslem4  25425  ipasslem5  25426  ipasslem8  25428  ipblnfi  25447  ip2eqi  25448  ubthlem1  25462  htthlem  25510  h2hmetdval  25571  axhvcom-zf  25576  axhis1-zf  25587  axhis4-zf  25590  hvm1neg  25625  hvsub4  25630  hvsubass  25637  hvsubdistr2  25643  hv2times  25654  hvsubcan  25667  hvsubcan2  25668  his2sub  25685  norm-i  25722  normpyc  25739  hhip  25770  hhph  25771  norm1exi  25844  hhssabloi  25854  hhssnv  25856  hhshsslem2  25860  hhssmetdval  25870  shscli  25911  shunssi  25962  shsleji  25964  shsidmi  25978  spanunsni  26173  h1datomi  26175  spansncvi  26246  pjss2i  26274  pjssmii  26275  pjocini  26292  homulid2  26395  honegdi  26404  ho2times  26414  nmopge0  26506  nmopgt0  26507  nmfnge0  26522  lnopaddi  26566  lnopmuli  26567  lnopsubi  26569  hmopbdoptHIL  26583  nmbdoplbi  26619  nmcoplbi  26623  nmophmi  26626  lnopconi  26629  lnfnaddi  26638  lnfnsubi  26641  nmbdfnlbi  26644  nmcfnlbi  26647  lnfnconi  26650  imaelshi  26653  cnlnadjlem2  26663  cnlnadjlem7  26668  nmoptrii  26689  nmopcoi  26690  adjcoi  26695  nmopcoadji  26696  bracnlnval  26709  leopmul  26729  opsqrlem1  26735  opsqrlem6  26740  hmopidmpji  26747  sto2i  26832  strlem1  26845  atcveq0  26943  atcv0eq  26974  atomli  26977  atcvati  26981  atcvat3i  26991  cdjreui  27027  cdj1i  27028  xdiv0  27293  xdivpnfrp  27297  mhmhmeotmd  27545  rezh  27588  qqhucn  27609  blscon  28329  cnllyscon  28330  ghomgrpilem2  28501  ghomsn  28503  sinccvglem  28513  fallrisefac  28724  wfrlem12  28931  frrlem11  28976  nobndlem8  29036  bpoly3  29397  fsumcube  29399  opnmbllem0  29627  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  voliunnfl  29635  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  opnrebl2  29716  heiborlem7  29916  rrnequiv  29934  ismrer1  29937  mapco2  30251  mzpaddmpt  30277  mzpmulmpt  30278  zindbi  30486  mpaaeu  30704  zringsubgval  32068  eel000cT  32571  eel0TT  32572  eel011  32575  eel012  32577  cnaddcom  33769
  Copyright terms: Public domain W3C validator