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  1358  mp3an12  1361  mp3an13  1362  ax9o  1744  sbnfc2  3185  ssdifss  3334  undifss  3572  uneqdifeqim  3577  elssuni  3915  csbexa  4212  difexg  4224  rabexg  4226  abssexg  4265  snexg  4267  copsexg  4329  sotritric  4414  sotritrieq  4415  trsuc  4512  oneli  4518  unexb  4532  opeluu  4540  rabxfr  4560  reuhyp  4562  ordunisuc2r  4605  reg3exmid  4671  brrelex12i  4760  brrelex1i  4761  brrelex2i  4762  xpss2  4829  opabid2  4852  eliunxp  4860  releldmi  4962  relelrni  4963  dmexg  4987  rnexg  4988  elres  5040  resexg  5044  relbrcnvg  5106  brcodir  5115  sotri  5123  sotri2  5125  sotri3  5126  dfrel2  5178  coi1  5243  fco  5488  fssres  5500  fabexg  5512  fvopab3g  5706  mptrcl  5716  mpteqb  5724  elfvmptrab1  5728  ffvelcdmi  5768  fsn2  5808  dfmptg  5813  fvpr1  5842  fvconst2  5854  mptexg  5863  oprabid  6032  ovprc  6036  caovcl  6159  caovass  6165  caovdi  6184  elmpocl  6199  ofexg  6221  resfunexgALT  6251  fo1stresm  6305  fo2ndresm  6306  1stexg  6311  2ndexg  6312  elopabi  6339  mpoexxg  6354  mpoxopn0yelv  6383  rntpos  6401  smores  6436  tfr0dm  6466  tfrlemibxssdm  6471  tfrexlem  6478  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  rdgruledefgg  6519  rdgruledefg  6520  rdgivallem  6525  rdgexg  6533  frec0g  6541  ordgt0ge1  6579  omfnex  6593  oeiv  6600  nna0r  6622  nnm0r  6623  nnsucsssuc  6636  nn2m  6671  nnaordex  6672  nnawordex  6673  ecdmn0m  6722  ecelqsi  6734  ecidg  6744  ectocl  6747  encv  6891  f1oen  6908  ssdomg  6928  map1  6963  fiprc  6966  xpdom1  6990  fict  7026  isinfinf  7055  ac6sfi  7056  xpfi  7090  en1eqsn  7111  fidcenumlemr  7118  fiss  7140  eqinfti  7183  djueq2  7204  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  djuf1olem  7216  djulclb  7218  inl11  7228  eldju1st  7234  1stinl  7237  2ndinl  7238  1stinr  7239  2ndinr  7240  ctssdccl  7274  isomnimap  7300  ismkvmap  7317  iswomnimap  7329  finacn  7382  djucomen  7394  exmidapne  7442  0nnq  7547  mulidnq  7572  archnqq  7600  prarloclemarch2  7602  nqnq0pi  7621  nq0m0r  7639  nq02m  7648  prarloclemlt  7676  prarloclemn  7682  prarloclem5  7683  addnqprllem  7710  addnqprulem  7711  appdivnq  7746  1idprl  7773  1idpru  7774  addextpr  7804  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemnbj  7850  caucvgprlemloc  7858  caucvgprprlemnbj  7876  caucvgprprlemloc  7886  caucvgprprlemaddq  7891  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemloc  7904  suplocexprlemlub  7907  0nsr  7932  ltsosr  7947  recexgt0sr  7956  prsrpos  7968  caucvgsr  7985  mappsrprg  7987  suplocsrlem  7991  mulresr  8021  axcnre  8064  axpre-ltwlin  8066  mullid  8140  0re  8142  axmulgt0  8214  ltnsym2  8233  eqlei  8236  ltnei  8246  muladd11  8275  cnegex  8320  0cnALT  8332  negcl  8342  negneg  8392  mul02  8529  mulm1  8542  lt0neg2  8612  le0neg2  8614  recexre  8721  recexgt0  8723  mulge0  8762  gt0ap0i  8770  recextlem1  8794  recexap  8796  recclapzi  8880  recap0apzi  8881  recidapzi  8882  divassapzi  8905  divmulapzi  8906  divdirapzi  8907  rerecclapzi  8919  ltp1  8987  recgt0i  9049  ltmul1i  9063  ltdiv1i  9064  ltmuldivi  9065  ltmul2i  9066  lemul1i  9067  lemul2i  9068  sup3exmid  9100  nngt1ne1  9141  nnrecre  9143  nn0ge0  9390  nn0addcl  9400  nn0mulcl  9401  zgt0ge1  9501  dfuzi  9553  eluzel2  9723  eluz2b1  9792  uz2m1nn  9796  elnn0dc  9802  elnndc  9803  nn01to3  9808  zq  9817  nnrecq  9836  rpge0  9858  rpreccl  9872  mnflt  9975  pnfnlt  9979  mnfle  9984  xrlelttr  9998  xrltletr  9999  xrletr  10000  xgepnf  10008  xlt0neg2  10031  xle0neg2  10033  xaddpnf2  10039  xaddmnf2  10041  xaddid2  10055  elioomnf  10160  ige3m2fz  10241  fzshftral  10300  ige2m1fz1  10301  1fv  10331  4fvwrd4  10332  rebtwn2zlemstep  10467  qbtwnxr  10472  btwnzge0  10515  zmodid2  10569  q2txmodxeq0  10601  frec2uzrand  10622  frecuzrdgtcl  10629  frecfzennn  10643  nn0ennn  10650  uzennn  10653  0exp  10791  sqgt0api  10842  subsq2  10864  qsqeqor  10867  bernneq  10877  faclbnd  10958  faclbnd2  10959  faclbnd3  10960  hashinfuni  10994  hashxp  11043  iswrdiz  11073  lsw0  11114  ccatlid  11136  s1leng  11152  s1fv  11154  s111  11159  pfx0g  11203  2shfti  11337  reim  11358  imcl  11360  crim  11364  caucvgre  11487  rennim  11508  resqrexlemdecn  11518  qabsor  11581  absimle  11590  sqrtthi  11625  sqrtcli  11626  sqrtgt0i  11627  sqrtmsqi  11628  sqrtsqi  11629  sqsqrti  11630  sqrtge0i  11631  absidi  11632  absnidi  11633  xrmaxiflemlub  11754  serclim0  11811  fsum2d  11941  fsumcnv  11943  fsumconst  11960  modfsummodlem1  11962  fsumabs  11971  binom11  11992  prodf1  12048  prodfclim1  12050  prodsnf  12098  fprod2d  12129  fprodcnv  12131  efzval  12189  eftlub  12196  efsep  12197  ef4p  12200  efgt1  12203  reef11  12205  sinf  12210  cosf  12211  efi4p  12223  sinneg  12232  cosneg  12233  efival  12238  efmival  12239  cos01gt0  12269  sin02gt0  12270  absefib  12277  efieq1re  12278  demoivre  12279  demoivreALT  12280  eirraplem  12283  0dvds  12317  odd2np1lem  12378  odd2np1  12379  even2n  12380  mod2eq0even  12384  2teven  12393  opoe  12401  omoe  12402  opeo  12403  omeo  12404  m1exp1  12407  bits0e  12455  bits0o  12456  bitsinv1  12468  gcd0id  12495  gcdid0  12496  1gcd  12508  lcmdvds  12596  isprm2lem  12633  isprm3  12635  prmgt1  12649  coprm  12661  isevengcd2  12675  isoddgcd1  12676  sqpweven  12692  2sqpwodd  12693  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem16  12797  pc2dvds  12848  oddprmdvds  12872  pockthi  12876  1arith2  12886  unennn  12963  ctinfomlemom  12993  qnnen  12997  ssnnctlemct  13012  strslfv  13072  strle1g  13134  1strbas  13145  tgval  13290  ismgmn0  13386  mulgval  13654  mulgfng  13656  mulg0  13657  mulg1  13661  mulg2  13663  isnsg  13734  ringidvalg  13919  issrg  13923  subrgpropd  14211  rrgval  14220  islmod  14249  scaffvalg  14264  islssm  14315  sraval  14395  mopnset  14510  metuex  14513  zrhval  14575  zrhvalg  14576  zrhex  14579  psrbag  14627  istopon  14681  eltg4i  14723  eltg3  14725  tg1  14727  tg2  14728  topnex  14754  cldrcl  14770  restsn  14848  lmrcl  14859  metflem  15017  xmetf  15018  ismet2  15022  xmeteq0  15027  xmettri2  15029  xmetpsmet  15037  xmetres2  15047  blfvalps  15053  blex  15055  blvalps  15056  blval  15057  blfps  15077  blf  15078  mopnval  15110  cnbl0  15202  cnblcld  15203  blssioo  15221  resubmet  15224  cncfmet  15260  cnplimcim  15335  cnlimcim  15339  cnlimc  15340  dvfgg  15356  dvfpm  15357  dvfcnpm  15358  dvcj  15377  dvmptfsum  15393  reeff1olem  15439  ef2kpi  15474  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  sinhalfpip  15488  sinhalfpim  15489  coshalfpip  15490  coshalfpim  15491  sincosq1sgn  15494  sinq12gt0  15498  sinkpi  15515  reeflog  15531  relogef  15532  logrpap0b  15544  loggt0b  15559  1cxp  15568  ecxp  15569  2logb9irrap  15645  0sgm  15653  lgsval2lem  15683  m1lgs  15758  1vgrex  15815  upgrfi  15896  umgredgnlp  15944  djucllem  16122  bdrabexg  16227  bdunexb  16241  peano5set  16261  speano5  16265  bj-omtrans  16277  dom1o  16314  pwf1oexmid  16324  nninfsellemeq  16339  iswomninnlem  16376