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  3836  csbexa  4130  difexg  4142  rabexg  4144  abssexg  4180  snexg  4182  copsexg  4242  sotritric  4322  sotritrieq  4323  trsuc  4420  oneli  4426  unexb  4440  opeluu  4448  rabxfr  4468  reuhyp  4470  ordunisuc2r  4511  reg3exmid  4577  brrelex12i  4666  brrelex1i  4667  brrelex2i  4668  xpss2  4735  opabid2  4755  eliunxp  4763  releldmi  4863  relelrni  4864  dmexg  4888  rnexg  4889  elres  4940  resexg  4944  relbrcnvg  5004  brcodir  5013  sotri  5021  sotri2  5023  sotri3  5024  dfrel2  5076  coi1  5141  fco  5378  fssres  5388  fabexg  5400  fvopab3g  5586  mptrcl  5595  mpteqb  5603  elfvmptrab1  5607  ffvelcdmi  5647  fsn2  5687  dfmptg  5692  fvpr1  5717  fvconst2  5729  mptexg  5738  oprabid  5902  ovprc  5905  caovcl  6024  caovass  6030  caovdi  6049  elmpocl  6064  ofexg  6082  resfunexgALT  6104  fo1stresm  6157  fo2ndresm  6158  1stexg  6163  2ndexg  6164  elopabi  6191  mpoexxg  6206  mpoxopn0yelv  6235  rntpos  6253  smores  6288  tfr0dm  6318  tfrlemibxssdm  6323  tfrexlem  6330  tfr1onlembxssdm  6339  tfrcllembxssdm  6352  rdgruledefgg  6371  rdgruledefg  6372  rdgivallem  6377  rdgexg  6385  frec0g  6393  ordgt0ge1  6431  omfnex  6445  oeiv  6452  nna0r  6474  nnm0r  6475  nnsucsssuc  6488  nn2m  6523  nnaordex  6524  nnawordex  6525  ecdmn0m  6572  ecelqsi  6584  ecidg  6594  ectocl  6597  encv  6741  f1oen  6754  ssdomg  6773  map1  6807  fiprc  6810  xpdom1  6830  fict  6863  isinfinf  6892  ac6sfi  6893  xpfi  6924  en1eqsn  6942  fidcenumlemr  6949  fiss  6971  eqinfti  7014  djueq2  7035  djulclr  7043  djurclr  7044  djulcl  7045  djurcl  7046  djuf1olem  7047  djulclb  7049  inl11  7059  eldju1st  7065  1stinl  7068  2ndinl  7069  1stinr  7070  2ndinr  7071  ctssdccl  7105  isomnimap  7130  ismkvmap  7147  iswomnimap  7159  djucomen  7210  exmidapne  7254  0nnq  7358  mulidnq  7383  archnqq  7411  prarloclemarch2  7413  nqnq0pi  7432  nq0m0r  7450  nq02m  7459  prarloclemlt  7487  prarloclemn  7493  prarloclem5  7494  addnqprllem  7521  addnqprulem  7522  appdivnq  7557  1idprl  7584  1idpru  7585  addextpr  7615  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  caucvgprlemnbj  7661  caucvgprlemloc  7669  caucvgprprlemnbj  7687  caucvgprprlemloc  7697  caucvgprprlemaddq  7702  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemloc  7715  suplocexprlemlub  7718  0nsr  7743  ltsosr  7758  recexgt0sr  7767  prsrpos  7779  caucvgsr  7796  mappsrprg  7798  suplocsrlem  7802  mulresr  7832  axcnre  7875  axpre-ltwlin  7877  mullid  7950  0re  7952  axmulgt0  8023  ltnsym2  8042  eqlei  8045  ltnei  8055  muladd11  8084  cnegex  8129  0cnALT  8141  negcl  8151  negneg  8201  mul02  8338  mulm1  8351  lt0neg2  8420  le0neg2  8422  recexre  8529  recexgt0  8531  mulge0  8570  gt0ap0i  8578  recextlem1  8602  recexap  8604  recclapzi  8688  recap0apzi  8689  recidapzi  8690  divassapzi  8713  divmulapzi  8714  divdirapzi  8715  rerecclapzi  8727  ltp1  8795  recgt0i  8857  ltmul1i  8871  ltdiv1i  8872  ltmuldivi  8873  ltmul2i  8874  lemul1i  8875  lemul2i  8876  sup3exmid  8908  nngt1ne1  8948  nnrecre  8950  nn0ge0  9195  nn0addcl  9205  nn0mulcl  9206  zgt0ge1  9305  dfuzi  9357  eluzel2  9527  eluz2b1  9595  uz2m1nn  9599  elnn0dc  9605  elnndc  9606  nn01to3  9611  zq  9620  nnrecq  9639  rpge0  9660  rpreccl  9674  mnflt  9777  pnfnlt  9781  mnfle  9786  xrlelttr  9800  xrltletr  9801  xrletr  9802  xgepnf  9810  xlt0neg2  9833  xle0neg2  9835  xaddpnf2  9841  xaddmnf2  9843  xaddid2  9857  elioomnf  9962  ige3m2fz  10042  fzshftral  10101  ige2m1fz1  10102  1fv  10132  4fvwrd4  10133  rebtwn2zlemstep  10246  qbtwnxr  10251  btwnzge0  10293  zmodid2  10345  q2txmodxeq0  10377  frec2uzrand  10398  frecuzrdgtcl  10405  frecfzennn  10419  nn0ennn  10426  uzennn  10429  0exp  10548  sqgt0api  10598  subsq2  10620  qsqeqor  10623  bernneq  10633  faclbnd  10712  faclbnd2  10713  faclbnd3  10714  hashinfuni  10748  hashxp  10797  2shfti  10831  reim  10852  imcl  10854  crim  10858  caucvgre  10981  rennim  11002  resqrexlemdecn  11012  qabsor  11075  absimle  11084  sqrtthi  11119  sqrtcli  11120  sqrtgt0i  11121  sqrtmsqi  11122  sqrtsqi  11123  sqsqrti  11124  sqrtge0i  11125  absidi  11126  absnidi  11127  xrmaxiflemlub  11247  serclim0  11304  fsum2d  11434  fsumcnv  11436  fsumconst  11453  modfsummodlem1  11455  fsumabs  11464  binom11  11485  prodf1  11541  prodfclim1  11543  prodsnf  11591  fprod2d  11622  fprodcnv  11624  efzval  11682  eftlub  11689  efsep  11690  ef4p  11693  efgt1  11696  reef11  11698  sinf  11703  cosf  11704  efi4p  11716  sinneg  11725  cosneg  11726  efival  11731  efmival  11732  cos01gt0  11761  sin02gt0  11762  absefib  11769  efieq1re  11770  demoivre  11771  demoivreALT  11772  eirraplem  11775  0dvds  11809  odd2np1lem  11867  odd2np1  11868  even2n  11869  mod2eq0even  11873  2teven  11882  opoe  11890  omoe  11891  opeo  11892  omeo  11893  m1exp1  11896  gcd0id  11970  gcdid0  11971  1gcd  11983  lcmdvds  12069  isprm2lem  12106  isprm3  12108  prmgt1  12122  coprm  12134  isevengcd2  12148  isoddgcd1  12149  sqpweven  12165  2sqpwodd  12166  pythagtriplem12  12265  pythagtriplem13  12266  pythagtriplem14  12267  pythagtriplem16  12269  pc2dvds  12319  oddprmdvds  12342  pockthi  12346  1arith2  12356  unennn  12388  ctinfomlemom  12418  qnnen  12422  ssnnctlemct  12437  strslfv  12497  strle1g  12555  1strbas  12566  ismgmn0  12707  mulgval  12914  mulgfng  12915  mulg0  12916  mulg1  12918  mulg2  12920  ringidvalg  13044  issrg  13048  istopon  13293  tgval  13331  eltg4i  13337  eltg3  13339  tg1  13341  tg2  13342  topnex  13368  cldrcl  13384  restsn  13462  lmrcl  13473  metflem  13631  xmetf  13632  ismet2  13636  xmeteq0  13641  xmettri2  13643  xmetpsmet  13651  xmetres2  13661  blfvalps  13667  blex  13669  blvalps  13670  blval  13671  blfps  13691  blf  13692  mopnval  13724  cnbl0  13816  cnblcld  13817  blssioo  13827  resubmet  13830  cncfmet  13861  cnplimcim  13918  cnlimcim  13922  cnlimc  13923  dvfgg  13939  dvfpm  13940  dvfcnpm  13941  dvcj  13955  reeff1olem  13974  ef2kpi  14009  sinperlem  14011  sin2kpi  14014  cos2kpi  14015  sinhalfpip  14023  sinhalfpim  14024  coshalfpip  14025  coshalfpim  14026  sincosq1sgn  14029  sinq12gt0  14033  sinkpi  14050  reeflog  14066  relogef  14067  logrpap0b  14079  loggt0b  14094  1cxp  14103  ecxp  14104  2logb9irrap  14177  lgsval2lem  14193  djucllem  14323  bdrabexg  14429  bdunexb  14443  peano5set  14463  speano5  14467  bj-omtrans  14479  pwf1oexmid  14520  nninfsellemeq  14534  iswomninnlem  14568