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  3189  ssdifss  3339  undifss  3577  uneqdifeqim  3582  elssuni  3926  csbexa  4223  difexg  4236  rabexg  4238  abssexg  4278  snexg  4280  copsexg  4342  sotritric  4427  sotritrieq  4428  trsuc  4525  oneli  4531  unexb  4545  opeluu  4553  rabxfr  4573  reuhyp  4575  ordunisuc2r  4618  reg3exmid  4684  brrelex12i  4774  brrelex1i  4775  brrelex2i  4776  xpss2  4843  opabid2  4867  eliunxp  4875  releldmi  4977  relelrni  4978  dmexg  5002  rnexg  5003  elres  5055  resexg  5059  relbrcnvg  5122  brcodir  5131  sotri  5139  sotri2  5141  sotri3  5142  dfrel2  5194  coi1  5259  fco  5507  fssres  5520  fabexg  5532  fvopab3g  5728  mptrcl  5738  mpteqb  5746  elfvmptrab1  5750  ffvelcdmi  5789  fsn2  5829  dfmptg  5835  fcof  5841  fvpr1  5866  fvconst2  5878  mptexg  5889  oprabid  6060  ovprc  6064  caovcl  6187  caovass  6193  caovdi  6212  elmpocl  6227  relmptopab  6234  ofexg  6249  resfunexgALT  6279  fo1stresm  6333  fo2ndresm  6334  1stexg  6339  2ndexg  6340  elopabi  6369  mpoexxg  6384  elmpom  6412  supp0  6416  mpoxopn0yelv  6448  rntpos  6466  smores  6501  tfr0dm  6531  tfrlemibxssdm  6536  tfrexlem  6543  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  rdgruledefgg  6584  rdgruledefg  6585  rdgivallem  6590  rdgexg  6598  frec0g  6606  ordgt0ge1  6646  omfnex  6660  oeiv  6667  nna0r  6689  nnm0r  6690  nnsucsssuc  6703  nn2m  6738  nnaordex  6739  nnawordex  6740  ecdmn0m  6789  ecelqsi  6801  ecidg  6811  ectocl  6814  encv  6958  f1oen  6975  ssdomg  6995  map1  7030  fiprc  7033  dom1o  7045  xpdom1  7062  fict  7098  isinfinf  7129  ac6sfi  7130  xpfi  7167  en1eqsn  7190  fidcenumlemr  7197  fiss  7219  eqinfti  7262  djueq2  7283  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  djuf1olem  7295  djulclb  7297  inl11  7307  eldju1st  7313  1stinl  7316  2ndinl  7317  1stinr  7318  2ndinr  7319  ctssdccl  7353  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  finacn  7462  djucomen  7474  exmidapne  7522  0nnq  7627  mulidnq  7652  archnqq  7680  prarloclemarch2  7682  nqnq0pi  7701  nq0m0r  7719  nq02m  7728  prarloclemlt  7756  prarloclemn  7762  prarloclem5  7763  addnqprllem  7790  addnqprulem  7791  appdivnq  7826  1idprl  7853  1idpru  7854  addextpr  7884  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemnbj  7930  caucvgprlemloc  7938  caucvgprprlemnbj  7956  caucvgprprlemloc  7966  caucvgprprlemaddq  7971  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemloc  7984  suplocexprlemlub  7987  0nsr  8012  ltsosr  8027  recexgt0sr  8036  prsrpos  8048  caucvgsr  8065  mappsrprg  8067  suplocsrlem  8071  mulresr  8101  axcnre  8144  axpre-ltwlin  8146  mullid  8220  0re  8222  axmulgt0  8293  ltnsym2  8312  eqlei  8315  ltnei  8325  muladd11  8354  cnegex  8399  0cnALT  8411  negcl  8421  negneg  8471  mul02  8608  mulm1  8621  lt0neg2  8691  le0neg2  8693  recexre  8800  recexgt0  8802  mulge0  8841  gt0ap0i  8849  recextlem1  8873  recexap  8875  recclapzi  8959  recap0apzi  8960  recidapzi  8961  divassapzi  8984  divmulapzi  8985  divdirapzi  8986  rerecclapzi  8998  ltp1  9066  recgt0i  9128  ltmul1i  9142  ltdiv1i  9143  ltmuldivi  9144  ltmul2i  9145  lemul1i  9146  lemul2i  9147  sup3exmid  9179  nngt1ne1  9220  nnrecre  9222  nn0ge0  9469  nn0addcl  9479  nn0mulcl  9480  zgt0ge1  9582  dfuzi  9634  eluzel2  9804  eluz2b1  9879  uz2m1nn  9883  elnn0dc  9889  elnndc  9890  nn01to3  9895  zq  9904  nnrecq  9923  rpge0  9945  rpreccl  9959  mnflt  10062  pnfnlt  10066  mnfle  10071  xrlelttr  10085  xrltletr  10086  xrletr  10087  xgepnf  10095  xlt0neg2  10118  xle0neg2  10120  xaddpnf2  10126  xaddmnf2  10128  xaddid2  10142  elioomnf  10247  ige3m2fz  10329  fzshftral  10388  ige2m1fz1  10389  1fv  10419  4fvwrd4  10420  rebtwn2zlemstep  10558  qbtwnxr  10563  btwnzge0  10606  zmodid2  10660  q2txmodxeq0  10692  frec2uzrand  10713  frecuzrdgtcl  10720  frecfzennn  10734  nn0ennn  10741  uzennn  10744  0exp  10882  sqgt0api  10933  subsq2  10955  qsqeqor  10958  bernneq  10968  faclbnd  11049  faclbnd2  11050  faclbnd3  11051  hashinfuni  11085  hashxp  11136  iswrdiz  11169  lsw0  11210  ccatlid  11232  s1leng  11250  s1fv  11252  s111  11257  pfx0g  11306  2shfti  11454  reim  11475  imcl  11477  crim  11481  caucvgre  11604  rennim  11625  resqrexlemdecn  11635  qabsor  11698  absimle  11707  sqrtthi  11742  sqrtcli  11743  sqrtgt0i  11744  sqrtmsqi  11745  sqrtsqi  11746  sqsqrti  11747  sqrtge0i  11748  absidi  11749  absnidi  11750  xrmaxiflemlub  11871  serclim0  11928  fsum2d  12059  fsumcnv  12061  fsumconst  12078  modfsummodlem1  12080  fsumabs  12089  binom11  12110  prodf1  12166  prodfclim1  12168  prodsnf  12216  fprod2d  12247  fprodcnv  12249  efzval  12307  eftlub  12314  efsep  12315  ef4p  12318  efgt1  12321  reef11  12323  sinf  12328  cosf  12329  efi4p  12341  sinneg  12350  cosneg  12351  efival  12356  efmival  12357  cos01gt0  12387  sin02gt0  12388  absefib  12395  efieq1re  12396  demoivre  12397  demoivreALT  12398  eirraplem  12401  0dvds  12435  odd2np1lem  12496  odd2np1  12497  even2n  12498  mod2eq0even  12502  2teven  12511  opoe  12519  omoe  12520  opeo  12521  omeo  12522  m1exp1  12525  bits0e  12573  bits0o  12574  bitsinv1  12586  gcd0id  12613  gcdid0  12614  1gcd  12626  lcmdvds  12714  isprm2lem  12751  isprm3  12753  prmgt1  12767  coprm  12779  isevengcd2  12793  isoddgcd1  12794  sqpweven  12810  2sqpwodd  12811  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem16  12915  pc2dvds  12966  oddprmdvds  12990  pockthi  12994  1arith2  13004  unennn  13081  ctinfomlemom  13111  qnnen  13115  ssnnctlemct  13130  strslfv  13190  strle1g  13252  1strbas  13263  tgval  13408  ismgmn0  13504  mulgval  13772  mulgfng  13774  mulg0  13775  mulg1  13779  mulg2  13781  isnsg  13852  ringidvalg  14038  issrg  14042  subrgpropd  14331  rrgval  14340  islmod  14370  scaffvalg  14385  islssm  14436  sraval  14516  mopnset  14631  metuex  14634  zrhval  14696  zrhvalg  14697  zrhex  14700  psrbag  14748  istopon  14807  eltg4i  14849  eltg3  14851  tg1  14853  tg2  14854  topnex  14880  cldrcl  14896  restsn  14974  lmrcl  14986  metflem  15143  xmetf  15144  ismet2  15148  xmeteq0  15153  xmettri2  15155  xmetpsmet  15163  xmetres2  15173  blfvalps  15179  blex  15181  blvalps  15182  blval  15183  blfps  15203  blf  15204  mopnval  15236  cnbl0  15328  cnblcld  15329  blssioo  15347  resubmet  15350  cncfmet  15386  cnplimcim  15461  cnlimcim  15465  cnlimc  15466  dvfgg  15482  dvfpm  15483  dvfcnpm  15484  dvcj  15503  dvmptfsum  15519  reeff1olem  15565  ef2kpi  15600  sinperlem  15602  sin2kpi  15605  cos2kpi  15606  sinhalfpip  15614  sinhalfpim  15615  coshalfpip  15616  coshalfpim  15617  sincosq1sgn  15620  sinq12gt0  15624  sinkpi  15641  reeflog  15657  relogef  15658  logrpap0b  15670  loggt0b  15685  1cxp  15694  ecxp  15695  2logb9irrap  15771  0sgm  15782  lgsval2lem  15812  m1lgs  15887  1vgrex  15944  upgrfi  16026  umgredgnlp  16076  wlkop  16272  clwwlkn0  16332  djucllem  16501  bdrabexg  16605  bdunexb  16619  peano5set  16639  speano5  16643  bj-omtrans  16655  pw1ninf  16694  pwf1oexmid  16704  nninfsellemeq  16723  iswomninnlem  16765