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  1335  mp3an12  1338  mp3an13  1339  ax9o  1709  sbnfc2  3142  ssdifss  3290  undifss  3528  uneqdifeqim  3533  elssuni  3864  csbexa  4159  difexg  4171  rabexg  4173  abssexg  4212  snexg  4214  copsexg  4274  sotritric  4356  sotritrieq  4357  trsuc  4454  oneli  4460  unexb  4474  opeluu  4482  rabxfr  4502  reuhyp  4504  ordunisuc2r  4547  reg3exmid  4613  brrelex12i  4702  brrelex1i  4703  brrelex2i  4704  xpss2  4771  opabid2  4794  eliunxp  4802  releldmi  4902  relelrni  4903  dmexg  4927  rnexg  4928  elres  4979  resexg  4983  relbrcnvg  5045  brcodir  5054  sotri  5062  sotri2  5064  sotri3  5065  dfrel2  5117  coi1  5182  fco  5420  fssres  5430  fabexg  5442  fvopab3g  5631  mptrcl  5641  mpteqb  5649  elfvmptrab1  5653  ffvelcdmi  5693  fsn2  5733  dfmptg  5738  fvpr1  5763  fvconst2  5775  mptexg  5784  oprabid  5951  ovprc  5954  caovcl  6075  caovass  6081  caovdi  6100  elmpocl  6115  ofexg  6137  resfunexgALT  6162  fo1stresm  6216  fo2ndresm  6217  1stexg  6222  2ndexg  6223  elopabi  6250  mpoexxg  6265  mpoxopn0yelv  6294  rntpos  6312  smores  6347  tfr0dm  6377  tfrlemibxssdm  6382  tfrexlem  6389  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  rdgruledefgg  6430  rdgruledefg  6431  rdgivallem  6436  rdgexg  6444  frec0g  6452  ordgt0ge1  6490  omfnex  6504  oeiv  6511  nna0r  6533  nnm0r  6534  nnsucsssuc  6547  nn2m  6582  nnaordex  6583  nnawordex  6584  ecdmn0m  6633  ecelqsi  6645  ecidg  6655  ectocl  6658  encv  6802  f1oen  6815  ssdomg  6834  map1  6868  fiprc  6871  xpdom1  6891  fict  6926  isinfinf  6955  ac6sfi  6956  xpfi  6988  en1eqsn  7009  fidcenumlemr  7016  fiss  7038  eqinfti  7081  djueq2  7102  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djuf1olem  7114  djulclb  7116  inl11  7126  eldju1st  7132  1stinl  7135  2ndinl  7136  1stinr  7137  2ndinr  7138  ctssdccl  7172  isomnimap  7198  ismkvmap  7215  iswomnimap  7227  djucomen  7278  exmidapne  7322  0nnq  7426  mulidnq  7451  archnqq  7479  prarloclemarch2  7481  nqnq0pi  7500  nq0m0r  7518  nq02m  7527  prarloclemlt  7555  prarloclemn  7561  prarloclem5  7562  addnqprllem  7589  addnqprulem  7590  appdivnq  7625  1idprl  7652  1idpru  7653  addextpr  7683  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemnbj  7729  caucvgprlemloc  7737  caucvgprprlemnbj  7755  caucvgprprlemloc  7765  caucvgprprlemaddq  7770  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemloc  7783  suplocexprlemlub  7786  0nsr  7811  ltsosr  7826  recexgt0sr  7835  prsrpos  7847  caucvgsr  7864  mappsrprg  7866  suplocsrlem  7870  mulresr  7900  axcnre  7943  axpre-ltwlin  7945  mullid  8019  0re  8021  axmulgt0  8093  ltnsym2  8112  eqlei  8115  ltnei  8125  muladd11  8154  cnegex  8199  0cnALT  8211  negcl  8221  negneg  8271  mul02  8408  mulm1  8421  lt0neg2  8490  le0neg2  8492  recexre  8599  recexgt0  8601  mulge0  8640  gt0ap0i  8648  recextlem1  8672  recexap  8674  recclapzi  8758  recap0apzi  8759  recidapzi  8760  divassapzi  8783  divmulapzi  8784  divdirapzi  8785  rerecclapzi  8797  ltp1  8865  recgt0i  8927  ltmul1i  8941  ltdiv1i  8942  ltmuldivi  8943  ltmul2i  8944  lemul1i  8945  lemul2i  8946  sup3exmid  8978  nngt1ne1  9019  nnrecre  9021  nn0ge0  9268  nn0addcl  9278  nn0mulcl  9279  zgt0ge1  9378  dfuzi  9430  eluzel2  9600  eluz2b1  9669  uz2m1nn  9673  elnn0dc  9679  elnndc  9680  nn01to3  9685  zq  9694  nnrecq  9713  rpge0  9735  rpreccl  9749  mnflt  9852  pnfnlt  9856  mnfle  9861  xrlelttr  9875  xrltletr  9876  xrletr  9877  xgepnf  9885  xlt0neg2  9908  xle0neg2  9910  xaddpnf2  9916  xaddmnf2  9918  xaddid2  9932  elioomnf  10037  ige3m2fz  10118  fzshftral  10177  ige2m1fz1  10178  1fv  10208  4fvwrd4  10209  rebtwn2zlemstep  10324  qbtwnxr  10329  btwnzge0  10372  zmodid2  10426  q2txmodxeq0  10458  frec2uzrand  10479  frecuzrdgtcl  10486  frecfzennn  10500  nn0ennn  10507  uzennn  10510  0exp  10648  sqgt0api  10699  subsq2  10721  qsqeqor  10724  bernneq  10734  faclbnd  10815  faclbnd2  10816  faclbnd3  10817  hashinfuni  10851  hashxp  10900  iswrdiz  10924  2shfti  10978  reim  10999  imcl  11001  crim  11005  caucvgre  11128  rennim  11149  resqrexlemdecn  11159  qabsor  11222  absimle  11231  sqrtthi  11266  sqrtcli  11267  sqrtgt0i  11268  sqrtmsqi  11269  sqrtsqi  11270  sqsqrti  11271  sqrtge0i  11272  absidi  11273  absnidi  11274  xrmaxiflemlub  11394  serclim0  11451  fsum2d  11581  fsumcnv  11583  fsumconst  11600  modfsummodlem1  11602  fsumabs  11611  binom11  11632  prodf1  11688  prodfclim1  11690  prodsnf  11738  fprod2d  11769  fprodcnv  11771  efzval  11829  eftlub  11836  efsep  11837  ef4p  11840  efgt1  11843  reef11  11845  sinf  11850  cosf  11851  efi4p  11863  sinneg  11872  cosneg  11873  efival  11878  efmival  11879  cos01gt0  11909  sin02gt0  11910  absefib  11917  efieq1re  11918  demoivre  11919  demoivreALT  11920  eirraplem  11923  0dvds  11957  odd2np1lem  12016  odd2np1  12017  even2n  12018  mod2eq0even  12022  2teven  12031  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1exp1  12045  gcd0id  12119  gcdid0  12120  1gcd  12132  lcmdvds  12220  isprm2lem  12257  isprm3  12259  prmgt1  12273  coprm  12285  isevengcd2  12299  isoddgcd1  12300  sqpweven  12316  2sqpwodd  12317  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem16  12420  pc2dvds  12471  oddprmdvds  12495  pockthi  12499  1arith2  12509  unennn  12557  ctinfomlemom  12587  qnnen  12591  ssnnctlemct  12606  strslfv  12666  strle1g  12727  1strbas  12738  tgval  12876  ismgmn0  12944  mulgval  13195  mulgfng  13197  mulg0  13198  mulg1  13202  mulg2  13204  isnsg  13275  ringidvalg  13460  issrg  13464  subrgpropd  13752  rrgval  13761  islmod  13790  scaffvalg  13805  islssm  13856  sraval  13936  mopnset  14051  metuex  14054  zrhval  14116  zrhvalg  14117  zrhex  14120  psrbag  14166  istopon  14192  eltg4i  14234  eltg3  14236  tg1  14238  tg2  14239  topnex  14265  cldrcl  14281  restsn  14359  lmrcl  14370  metflem  14528  xmetf  14529  ismet2  14533  xmeteq0  14538  xmettri2  14540  xmetpsmet  14548  xmetres2  14558  blfvalps  14564  blex  14566  blvalps  14567  blval  14568  blfps  14588  blf  14589  mopnval  14621  cnbl0  14713  cnblcld  14714  blssioo  14732  resubmet  14735  cncfmet  14771  cnplimcim  14846  cnlimcim  14850  cnlimc  14851  dvfgg  14867  dvfpm  14868  dvfcnpm  14869  dvcj  14888  dvmptfsum  14904  reeff1olem  14947  ef2kpi  14982  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  sinhalfpip  14996  sinhalfpim  14997  coshalfpip  14998  coshalfpim  14999  sincosq1sgn  15002  sinq12gt0  15006  sinkpi  15023  reeflog  15039  relogef  15040  logrpap0b  15052  loggt0b  15067  1cxp  15076  ecxp  15077  2logb9irrap  15150  lgsval2lem  15167  m1lgs  15242  djucllem  15362  bdrabexg  15468  bdunexb  15482  peano5set  15502  speano5  15506  bj-omtrans  15518  pwf1oexmid  15560  nninfsellemeq  15574  iswomninnlem  15609