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  1324  mp3an12  1327  mp3an13  1328  ax9o  1698  sbnfc2  3117  ssdifss  3265  undifss  3503  uneqdifeqim  3508  elssuni  3835  csbexa  4129  difexg  4141  rabexg  4143  abssexg  4179  snexg  4181  copsexg  4241  sotritric  4321  sotritrieq  4322  trsuc  4419  oneli  4425  unexb  4439  opeluu  4447  rabxfr  4467  reuhyp  4469  ordunisuc2r  4510  reg3exmid  4576  brrelex12i  4665  brrelex1i  4666  brrelex2i  4667  xpss2  4734  opabid2  4754  eliunxp  4762  releldmi  4862  relelrni  4863  dmexg  4887  rnexg  4888  elres  4939  resexg  4943  relbrcnvg  5003  brcodir  5012  sotri  5020  sotri2  5022  sotri3  5023  dfrel2  5075  coi1  5140  fco  5377  fssres  5387  fabexg  5399  fvopab3g  5585  mptrcl  5594  mpteqb  5602  elfvmptrab1  5606  ffvelcdmi  5646  fsn2  5686  dfmptg  5691  fvpr1  5716  fvconst2  5728  mptexg  5737  oprabid  5901  ovprc  5904  caovcl  6023  caovass  6029  caovdi  6048  elmpocl  6063  ofexg  6081  resfunexgALT  6103  fo1stresm  6156  fo2ndresm  6157  1stexg  6162  2ndexg  6163  elopabi  6190  mpoexxg  6205  mpoxopn0yelv  6234  rntpos  6252  smores  6287  tfr0dm  6317  tfrlemibxssdm  6322  tfrexlem  6329  tfr1onlembxssdm  6338  tfrcllembxssdm  6351  rdgruledefgg  6370  rdgruledefg  6371  rdgivallem  6376  rdgexg  6384  frec0g  6392  ordgt0ge1  6430  omfnex  6444  oeiv  6451  nna0r  6473  nnm0r  6474  nnsucsssuc  6487  nn2m  6522  nnaordex  6523  nnawordex  6524  ecdmn0m  6571  ecelqsi  6583  ecidg  6593  ectocl  6596  encv  6740  f1oen  6753  ssdomg  6772  map1  6806  fiprc  6809  xpdom1  6829  fict  6862  isinfinf  6891  ac6sfi  6892  xpfi  6923  en1eqsn  6941  fidcenumlemr  6948  fiss  6970  eqinfti  7013  djueq2  7034  djulclr  7042  djurclr  7043  djulcl  7044  djurcl  7045  djuf1olem  7046  djulclb  7048  inl11  7058  eldju1st  7064  1stinl  7067  2ndinl  7068  1stinr  7069  2ndinr  7070  ctssdccl  7104  isomnimap  7129  ismkvmap  7146  iswomnimap  7158  djucomen  7209  exmidapne  7250  0nnq  7354  mulidnq  7379  archnqq  7407  prarloclemarch2  7409  nqnq0pi  7428  nq0m0r  7446  nq02m  7455  prarloclemlt  7483  prarloclemn  7489  prarloclem5  7490  addnqprllem  7517  addnqprulem  7518  appdivnq  7553  1idprl  7580  1idpru  7581  addextpr  7611  cauappcvgprlemdisj  7641  cauappcvgprlemloc  7642  cauappcvgprlemladdru  7646  cauappcvgprlemladdrl  7647  caucvgprlemnbj  7657  caucvgprlemloc  7665  caucvgprprlemnbj  7683  caucvgprprlemloc  7693  caucvgprprlemaddq  7698  suplocexprlemmu  7708  suplocexprlemru  7709  suplocexprlemloc  7711  suplocexprlemlub  7714  0nsr  7739  ltsosr  7754  recexgt0sr  7763  prsrpos  7775  caucvgsr  7792  mappsrprg  7794  suplocsrlem  7798  mulresr  7828  axcnre  7871  axpre-ltwlin  7873  mulid2  7946  0re  7948  axmulgt0  8019  ltnsym2  8038  eqlei  8041  ltnei  8051  muladd11  8080  cnegex  8125  0cnALT  8137  negcl  8147  negneg  8197  mul02  8334  mulm1  8347  lt0neg2  8416  le0neg2  8418  recexre  8525  recexgt0  8527  mulge0  8566  gt0ap0i  8574  recextlem1  8597  recexap  8599  recclapzi  8683  recap0apzi  8684  recidapzi  8685  divassapzi  8708  divmulapzi  8709  divdirapzi  8710  rerecclapzi  8722  ltp1  8790  recgt0i  8852  ltmul1i  8866  ltdiv1i  8867  ltmuldivi  8868  ltmul2i  8869  lemul1i  8870  lemul2i  8871  sup3exmid  8903  nngt1ne1  8943  nnrecre  8945  nn0ge0  9190  nn0addcl  9200  nn0mulcl  9201  zgt0ge1  9300  dfuzi  9352  eluzel2  9522  eluz2b1  9590  uz2m1nn  9594  elnn0dc  9600  elnndc  9601  nn01to3  9606  zq  9615  nnrecq  9634  rpge0  9653  rpreccl  9667  mnflt  9770  pnfnlt  9774  mnfle  9779  xrlelttr  9793  xrltletr  9794  xrletr  9795  xgepnf  9803  xlt0neg2  9826  xle0neg2  9828  xaddpnf2  9834  xaddmnf2  9836  xaddid2  9850  elioomnf  9955  ige3m2fz  10035  fzshftral  10094  ige2m1fz1  10095  1fv  10125  4fvwrd4  10126  rebtwn2zlemstep  10239  qbtwnxr  10244  btwnzge0  10286  zmodid2  10338  q2txmodxeq0  10370  frec2uzrand  10391  frecuzrdgtcl  10398  frecfzennn  10412  nn0ennn  10419  uzennn  10422  0exp  10541  sqgt0api  10591  subsq2  10613  qsqeqor  10616  bernneq  10626  faclbnd  10705  faclbnd2  10706  faclbnd3  10707  hashinfuni  10741  hashxp  10790  2shfti  10824  reim  10845  imcl  10847  crim  10851  caucvgre  10974  rennim  10995  resqrexlemdecn  11005  qabsor  11068  absimle  11077  sqrtthi  11112  sqrtcli  11113  sqrtgt0i  11114  sqrtmsqi  11115  sqrtsqi  11116  sqsqrti  11117  sqrtge0i  11118  absidi  11119  absnidi  11120  xrmaxiflemlub  11240  serclim0  11297  fsum2d  11427  fsumcnv  11429  fsumconst  11446  modfsummodlem1  11448  fsumabs  11457  binom11  11478  prodf1  11534  prodfclim1  11536  prodsnf  11584  fprod2d  11615  fprodcnv  11617  efzval  11675  eftlub  11682  efsep  11683  ef4p  11686  efgt1  11689  reef11  11691  sinf  11696  cosf  11697  efi4p  11709  sinneg  11718  cosneg  11719  efival  11724  efmival  11725  cos01gt0  11754  sin02gt0  11755  absefib  11762  efieq1re  11763  demoivre  11764  demoivreALT  11765  eirraplem  11768  0dvds  11802  odd2np1lem  11860  odd2np1  11861  even2n  11862  mod2eq0even  11866  2teven  11875  opoe  11883  omoe  11884  opeo  11885  omeo  11886  m1exp1  11889  gcd0id  11963  gcdid0  11964  1gcd  11976  lcmdvds  12062  isprm2lem  12099  isprm3  12101  prmgt1  12115  coprm  12127  isevengcd2  12141  isoddgcd1  12142  sqpweven  12158  2sqpwodd  12159  pythagtriplem12  12258  pythagtriplem13  12259  pythagtriplem14  12260  pythagtriplem16  12262  pc2dvds  12312  oddprmdvds  12335  pockthi  12339  1arith2  12349  unennn  12381  ctinfomlemom  12411  qnnen  12415  ssnnctlemct  12430  strslfv  12489  strle1g  12546  1strbas  12555  ismgmn0  12669  mulgval  12875  mulgfng  12876  mulg0  12877  mulg1  12879  mulg2  12881  ringidvalg  12970  issrg  12974  istopon  13178  tgval  13216  eltg4i  13222  eltg3  13224  tg1  13226  tg2  13227  topnex  13253  cldrcl  13269  restsn  13347  lmrcl  13358  metflem  13516  xmetf  13517  ismet2  13521  xmeteq0  13526  xmettri2  13528  xmetpsmet  13536  xmetres2  13546  blfvalps  13552  blex  13554  blvalps  13555  blval  13556  blfps  13576  blf  13577  mopnval  13609  cnbl0  13701  cnblcld  13702  blssioo  13712  resubmet  13715  cncfmet  13746  cnplimcim  13803  cnlimcim  13807  cnlimc  13808  dvfgg  13824  dvfpm  13825  dvfcnpm  13826  dvcj  13840  reeff1olem  13859  ef2kpi  13894  sinperlem  13896  sin2kpi  13899  cos2kpi  13900  sinhalfpip  13908  sinhalfpim  13909  coshalfpip  13910  coshalfpim  13911  sincosq1sgn  13914  sinq12gt0  13918  sinkpi  13935  reeflog  13951  relogef  13952  logrpap0b  13964  loggt0b  13979  1cxp  13988  ecxp  13989  2logb9irrap  14062  lgsval2lem  14078  djucllem  14208  bdrabexg  14314  bdunexb  14328  peano5set  14348  speano5  14352  bj-omtrans  14364  pwf1oexmid  14405  nninfsellemeq  14419  iswomninnlem  14453