Theorem mpan 424

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpan.1	|- ph
mpan.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan	|- ( ps -> ch )

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 |- ph
2	1	a1i 9	. 2 |- ( ps -> ph )
3		mpan.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpancom 422	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mp2an  426  mpanl12  436  mp3an1  1361  mp3an12  1364  mp3an13  1365  ax9o  1746  sbnfc2  3199  ssdifss  3349  undifss  3590  uneqdifeqim  3595  elssuni  3942  csbexa  4239  difexg  4252  rabexg  4255  abssexg  4295  snexg  4297  copsexg  4360  sotritric  4445  sotritrieq  4446  trsuc  4543  oneli  4549  unexb  4563  opeluu  4571  rabxfr  4591  reuhyp  4593  ordunisuc2r  4636  reg3exmid  4702  brrelex12i  4792  brrelex1i  4793  brrelex2i  4794  xpss2  4861  opabid2  4886  eliunxp  4894  releldmi  4996  relelrni  4997  dmexg  5021  rnexg  5022  elres  5074  resexg  5078  relbrcnvg  5141  brcodir  5150  sotri  5158  sotri2  5160  sotri3  5161  dfrel2  5213  coi1  5278  fco  5527  fssres  5540  fabexg  5554  fvopab3g  5750  mptrcl  5760  mpteqb  5768  elfvmptrab1  5772  ffvelcdmi  5811  fsn2  5851  dfmptg  5857  fcof  5863  fvpr1  5888  fvconst2  5900  mptexg  5911  oprabid  6082  ovprc  6086  caovcl  6209  caovass  6215  caovdi  6234  elmpocl  6249  relmptopab  6256  ofexg  6271  resfunexgALT  6301  fo1stresm  6355  fo2ndresm  6356  1stexg  6361  2ndexg  6362  elopabi  6391  mpoexxg  6406  elmpom  6434  supp0  6438  mpoxopn0yelv  6470  rntpos  6488  smores  6523  tfr0dm  6553  tfrlemibxssdm  6558  tfrexlem  6565  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  rdgruledefgg  6606  rdgruledefg  6607  rdgivallem  6612  rdgexg  6620  frec0g  6628  ordgt0ge1  6668  omfnex  6682  oeiv  6689  nna0r  6711  nnm0r  6712  nnsucsssuc  6725  nn2m  6760  nnaordex  6761  nnawordex  6762  ecdmn0m  6811  ecelqsi  6823  ecidg  6833  ectocl  6836  encv  6981  f1oen  6998  ssdomg  7018  map1  7054  fiprc  7057  dom1o  7069  xpdom1  7086  fict  7123  isinfinf  7154  ac6sfi  7155  xpfi  7192  en1eqsn  7218  fidcenumlemr  7225  fiss  7264  fipwfi  7272  eqinfti  7311  djueq2  7332  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djuf1olem  7344  djulclb  7346  inl11  7356  eldju1st  7362  1stinl  7365  2ndinl  7366  1stinr  7367  2ndinr  7368  ctssdccl  7402  isomnimap  7428  ismkvmap  7445  iswomnimap  7457  finacn  7511  djucomen  7523  exmidapne  7574  0nnq  7679  mulidnq  7704  archnqq  7732  prarloclemarch2  7734  nqnq0pi  7753  nq0m0r  7771  nq02m  7780  prarloclemlt  7808  prarloclemn  7814  prarloclem5  7815  addnqprllem  7842  addnqprulem  7843  appdivnq  7878  1idprl  7905  1idpru  7906  addextpr  7936  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemnbj  7982  caucvgprlemloc  7990  caucvgprprlemnbj  8008  caucvgprprlemloc  8018  caucvgprprlemaddq  8023  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemloc  8036  suplocexprlemlub  8039  0nsr  8064  ltsosr  8079  recexgt0sr  8088  prsrpos  8100  caucvgsr  8117  mappsrprg  8119  suplocsrlem  8123  mulresr  8153  axcnre  8196  axpre-ltwlin  8198  mullid  8272  0re  8274  axmulgt0  8345  ltnsym2  8364  eqlei  8367  ltnei  8377  muladd11  8406  cnegex  8451  0cnALT  8463  negcl  8473  negneg  8523  mul02  8660  mulm1  8673  lt0neg2  8743  le0neg2  8745  recexre  8852  recexgt0  8854  mulge0  8893  gt0ap0i  8901  recextlem1  8925  recexap  8927  recclapzi  9011  recap0apzi  9012  recidapzi  9013  divassapzi  9036  divmulapzi  9037  divdirapzi  9038  rerecclapzi  9050  ltp1  9118  recgt0i  9180  ltmul1i  9194  ltdiv1i  9195  ltmuldivi  9196  ltmul2i  9197  lemul1i  9198  lemul2i  9199  sup3exmid  9231  nngt1ne1  9272  nnrecre  9274  nn0ge0  9521  nn0addcl  9531  nn0mulcl  9532  zgt0ge1  9636  dfuzi  9688  eluzel2  9858  eluz2b1  9933  uz2m1nn  9937  elnn0dc  9943  elnndc  9944  nn01to3  9949  zq  9958  nnrecq  9977  rpge0  9999  rpreccl  10013  mnflt  10116  pnfnlt  10120  mnfle  10125  xrlelttr  10139  xrltletr  10140  xrletr  10141  xgepnf  10149  xlt0neg2  10172  xle0neg2  10174  xaddpnf2  10180  xaddmnf2  10182  xaddid2  10196  elioomnf  10301  ige3m2fz  10383  fzshftral  10442  ige2m1fz1  10443  1fv  10473  4fvwrd4  10474  rebtwn2zlemstep  10612  qbtwnxr  10617  btwnzge0  10660  zmodid2  10714  q2txmodxeq0  10746  frec2uzrand  10767  frecuzrdgtcl  10774  frecfzennn  10788  nn0ennn  10795  uzennn  10798  0exp  10936  sqgt0api  10987  subsq2  11009  qsqeqor  11012  bernneq  11022  faclbnd  11103  faclbnd2  11104  faclbnd3  11105  hashinfuni  11140  hashxp  11191  hashpwfi  11193  iswrdiz  11231  lsw0  11272  ccatlid  11294  s1leng  11312  s1fv  11314  s111  11319  pfx0g  11368  2shfti  11516  reim  11537  imcl  11539  crim  11543  caucvgre  11666  rennim  11687  resqrexlemdecn  11697  qabsor  11760  absimle  11769  sqrtthi  11804  sqrtcli  11805  sqrtgt0i  11806  sqrtmsqi  11807  sqrtsqi  11808  sqsqrti  11809  sqrtge0i  11810  absidi  11811  absnidi  11812  xrmaxiflemlub  11933  serclim0  11990  fsum2d  12121  fsumcnv  12123  fsumconst  12140  modfsummodlem1  12142  fsumabs  12151  binom11  12172  prodf1  12228  prodfclim1  12230  prodsnf  12278  fprod2d  12309  fprodcnv  12311  efzval  12369  eftlub  12376  efsep  12377  ef4p  12380  efgt1  12383  reef11  12385  sinf  12390  cosf  12391  efi4p  12403  sinneg  12412  cosneg  12413  efival  12418  efmival  12419  cos01gt0  12449  sin02gt0  12450  absefib  12457  efieq1re  12458  demoivre  12459  demoivreALT  12460  eirraplem  12463  0dvds  12497  odd2np1lem  12558  odd2np1  12559  even2n  12560  mod2eq0even  12564  2teven  12573  opoe  12581  omoe  12582  opeo  12583  omeo  12584  m1exp1  12587  bits0e  12635  bits0o  12636  bitsinv1  12648  gcd0id  12675  gcdid0  12676  1gcd  12688  lcmdvds  12776  isprm2lem  12813  isprm3  12815  prmgt1  12829  coprm  12841  isevengcd2  12855  isoddgcd1  12856  sqpweven  12872  2sqpwodd  12873  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem16  12977  pc2dvds  13028  oddprmdvds  13052  pockthi  13056  1arith2  13066  unennn  13148  ctinfomlemom  13178  qnnen  13182  ssnnctlemct  13197  strslfv  13257  strle1g  13319  1strbas  13330  tgval  13475  ismgmn0  13571  mulgval  13839  mulgfng  13841  mulg0  13842  mulg1  13846  mulg2  13848  isnsg  13919  ringidvalg  14105  issrg  14109  subrgpropd  14398  rrgval  14407  islmod  14439  scaffvalg  14454  islssm  14505  sraval  14585  mopnset  14700  metuex  14703  zrhval  14765  zrhvalg  14766  zrhex  14769  psrbag  14817  psrbagaddclfi  14825  istopon  14878  eltg4i  14920  eltg3  14922  tg1  14924  tg2  14925  topnex  14951  cldrcl  14967  restsn  15045  lmrcl  15057  metflem  15214  xmetf  15215  ismet2  15219  xmeteq0  15224  xmettri2  15226  xmetpsmet  15234  xmetres2  15244  blfvalps  15250  blex  15252  blvalps  15253  blval  15254  blfps  15274  blf  15275  mopnval  15307  cnbl0  15399  cnblcld  15400  blssioo  15418  resubmet  15421  cncfmet  15457  cnplimcim  15532  cnlimcim  15536  cnlimc  15537  dvfgg  15553  dvfpm  15554  dvfcnpm  15555  dvcj  15574  dvmptfsum  15590  reeff1olem  15636  ef2kpi  15671  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  sinhalfpip  15685  sinhalfpim  15686  coshalfpip  15687  coshalfpim  15688  sincosq1sgn  15691  sinq12gt0  15695  sinkpi  15712  reeflog  15728  relogef  15729  logrpap0b  15741  loggt0b  15756  1cxp  15765  ecxp  15766  2logb9irrap  15842  0sgm  15853  lgsval2lem  15883  m1lgs  15958  1vgrex  16015  upgrfi  16097  umgredgnlp  16147  wlkop  16343  clwwlkn0  16403  djucllem  16572  bdrabexg  16676  bdunexb  16690  peano5set  16710  speano5  16714  bj-omtrans  16726  pw1ninf  16765  pwf1oexmid  16773  nninfsellemeq  16792  iswomninnlem  16834