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

Theorem mp3an1 1266
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 1154 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 652 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mp3an12  1269  mp3an1i  1272  mp3anl1  1273  mp3an  1279  onint  4734  tfrlem9  6605  oaord1  6753  oaword2  6755  oawordeulem  6756  oa00  6761  omword1  6775  omword2  6776  omlimcl  6780  oeoelem  6800  nnaordex  6840  enp1i  7302  unfilem2  7331  dffi3  7394  unbnn3  7569  pwcdaen  8021  ackbij1b  8075  zorn2  8342  zornn0  8344  ttukey  8354  brdom7disj  8365  brdom6disj  8366  wunex2  8569  muladd11  9192  00id  9197  mul02  9200  negsubdi  9313  mulneg1  9426  ltaddpos  9474  addge01  9494  reccl  9641  recid  9648  recid2  9649  recdiv2  9683  divdiv23zi  9723  ltmul12a  9822  lemul12a  9824  mulgt1  9825  ltmulgt11  9826  gt0div  9832  ge0div  9833  lediv12a  9859  ledivp1  9868  ltdiv23i  9891  ledivp1i  9892  ltdivp1i  9893  infm3  9923  infmrcl  9943  nngt1ne1  9983  8th4div3  10147  gtndiv  10303  nn0ind  10322  fnn0ind  10325  supminf  10519  xrre2  10714  qsqueeze  10743  xmulpnf1  10809  xlemul1a  10823  xrub  10846  ioorebas  10962  expubnd  11395  le2sq2  11412  crreczi  11459  bernneq  11460  faclbnd5  11544  faclbnd6  11545  bccl  11568  hashbc  11657  ccatlid  11703  shftfval  11840  mulre  11881  sqrlem4  12006  sqrlem7  12009  sqreulem  12118  binom1p  12565  0.999...  12613  efsub  12656  efi4p  12693  sinadd  12720  cosadd  12721  cos2t  12734  cos2tsin  12735  sin01gt0  12746  cos01gt0  12747  absefib  12754  efieq1re  12755  demoivreALT  12757  rpnnen2lem4  12772  odd2np1  12863  divalglem0  12868  divalglem4  12871  divalglem9  12876  gcdcllem3  12968  gcdn0gt0  12977  gcdadd  12985  gcdmultiple  13005  algcvgblem  13023  algcvga  13025  isprm3  13043  coprm  13055  divgcdodd  13074  phibndlem  13114  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pythagtriplem4  13148  pythagtriplem11  13154  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  infpn2  13236  1arith2  13251  vdwap0  13299  vdwap1  13300  ipolt  14540  gsumval2a  14737  mplsubrglem  16457  cnfldneg  16682  cnflddiv  16686  cnfldmulg  16688  cnfldexp  16689  thlleval  16880  neiptoptop  17150  iccordt  17232  divstgplem  18103  bl2ioo  18776  ioo2blex  18778  blssioo  18779  tgioo  18780  xrsblre  18795  iccntr  18805  icccmplem3  18808  reconnlem2  18811  opnreen  18815  iccpnfcnv  18922  cnllycmp  18934  pcoptcl  18999  ovolmge0  19326  ovolctb2  19341  ismbl2  19376  cmmbl  19382  nulmbl  19383  unmbl  19385  voliunlem1  19397  voliunlem2  19398  ioombl1  19409  opnmbllem  19446  mbfima  19477  i1fsub  19553  itg1sub  19554  ellimc3  19719  limcflf  19721  dvcnvre  19856  coe1termlem  20129  dgrsub  20143  dvnply2  20157  dvnply  20158  reeff1o  20316  sinperlem  20341  sincosq1eq  20373  resinf1o  20391  logeftb  20431  logge0  20453  logdivlti  20468  efopn  20502  logtayl2  20506  loglesqr  20595  logrec  20614  xrlimcnp  20760  ppinncl  20910  chtrpcl  20911  bposlem2  21022  bposlem8  21028  lgsdir2  21065  1lgs  21074  redwlklem  21558  isgrpoi  21739  grpo2grp  21775  imsmetlem  22135  nmcvcn  22144  ipval2  22156  lnocoi  22211  nmlno0lem  22247  nmblolbii  22253  blometi  22257  blocnilem  22258  blocni  22259  ipasslem1  22285  ipasslem2  22286  ipasslem4  22288  ipasslem5  22289  ipasslem8  22291  ipblnfi  22310  ip2eqi  22311  ubthlem1  22325  htthlem  22373  h2hmetdval  22434  axhvcom-zf  22439  axhis1-zf  22450  axhis4-zf  22453  hvm1neg  22487  hvsub4  22492  hvsubass  22499  hvsubdistr2  22505  hv2times  22516  hvsubcan  22529  hvsubcan2  22530  his2sub  22547  norm-i  22584  normpyc  22601  hhip  22632  hhph  22633  norm1exi  22705  hhssabloi  22715  hhssnv  22717  hhshsslem2  22721  hhssmetdval  22731  shscli  22772  shunssi  22823  shsleji  22825  shsidmi  22839  spanunsni  23034  h1datomi  23036  spansncvi  23107  pjss2i  23135  pjssmii  23136  pjocini  23153  homulid2  23256  honegdi  23265  ho2times  23275  nmopge0  23367  nmopgt0  23368  nmfnge0  23383  lnopaddi  23427  lnopmuli  23428  lnopsubi  23430  hmopbdoptHIL  23444  nmbdoplbi  23480  nmcoplbi  23484  nmophmi  23487  lnopconi  23490  lnfnaddi  23499  lnfnsubi  23502  nmbdfnlbi  23505  nmcfnlbi  23508  lnfnconi  23511  imaelshi  23514  cnlnadjlem2  23524  cnlnadjlem7  23529  nmoptrii  23550  nmopcoi  23551  adjcoi  23556  nmopcoadji  23557  bracnlnval  23570  leopmul  23590  opsqrlem1  23596  opsqrlem6  23601  hmopidmpji  23608  sto2i  23693  strlem1  23706  atcveq0  23804  atcv0eq  23835  atomli  23838  atcvati  23842  atcvat3i  23852  cdjreui  23888  cdj1i  23889  xdiv0  24128  xdivpnfrp  24132  zzsmulg  24218  remulg  24223  mhmhmeotmd  24266  rezh  24308  qqhucn  24329  blscon  24884  cnllyscon  24885  ghomgrpilem2  25050  ghomsn  25052  sinccvglem  25062  fallrisefac  25293  wfrlem12  25481  frrlem11  25507  nobndlem8  25567  brbtwn2  25748  colinearalglem4  25752  ax5seglem1  25771  ax5seglem2  25772  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  bpoly3  26008  fsumcube  26010  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  voliunnfl  26149  opnrebl2  26214  heiborlem7  26416  rrnequiv  26434  ismrer1  26437  mapco2  26660  mzpaddmpt  26688  mzpmulmpt  26689  zindbi  26899  frlmsslsp  27116  mpaaeu  27223  f1otrspeq  27258  elfzelfzelfz  27981  sgnp  28234  eel000cT  28515  eel0TT  28516  eel011  28519  eel012  28521  cnaddcom  29454
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator