Theorem mpan 694

Description: An inference based on modus ponens.

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	. 2 |- ph
2		mpan.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	ex 373	. 2 |- (ph -> (ps -> ch))
4	1, 3	ax-mp 7	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mp2an 696  mpanl1 705  mpanl12 707  mp3an1 901  mp3an12 904  mp3an13 905  sbcbii 1974  sbcel12g 2007  sbceqdig 2008  csbie2t 2029  csbnestg 2032  csbabg 2039  ssdifss 2164  elssuni 2521  difexg 2717  rabexg 2719  unipw 2751  sspwuni 2753  unexb 2868  difex2 2872  opeluu 2874  uniexb 2902  fr2nr 2920  fr3nr 2921  onminsb 3004  onminesb 3005  onintrab 3008  onnminsb 3011  onminex 3015  onel 3093  onuninsuc 3103  limuni3 3118  on0eqelt 3119  dfom2 3128  tfindsg2 3158  brrelexi 3203  relsn 3249  xpexg 3254  opabid2 3262  brelrn 3339  dmexg 3352  rnexg 3353  resiexg 3388  imaexg 3408  soirri 3434  sotri 3435  dfrel2 3477  coi1 3502  cnvexg 3511  coexg 3516  resfunexg 3571  cofunexg 3572  opabex2g 3603  fssxp 3628  fssres 3634  fcoi1 3636  fcoi2 3637  fabexg 3644  f1oabexg 3691  fvopab3 3768  fvimacnv 3796  ffvelrni 3806  rnssopab 3816  fopabco 3823  fopabcos 3824  fvconst2 3837  rdgsucopab 3937  rdglim2 3940  frsucopab 3945  tz7.48lem 3946  tz7.48-1 3947  tz7.48-2 3948  tz7.49 3950  tz7.49c 3951  abianfplem 3952  abianfp 3953  oprabex2g 4011  oprabval 4014  ndmopr 4037  1stcof 4091  elopabi 4107  eloprabi 4108  ordgt0ge1 4134  oe0m 4147  oa0r 4163  om0r 4164  om1r 4167  oe1m 4169  oawordeulem 4178  oaass 4185  odi 4200  omass 4201  oneo 4202  oen0 4203  oewordi 4208  oewordri 4209  oaabslem 4241  oaabs 4242  mapex 4318  map0 4334  ixpexg 4348  f1oen 4385  ssdomg 4395  snfi 4419  undom 4424  xpdom3 4431  mapdom2 4480  pwen 4489  limenpsi 4491  limensuci 4492  php 4499  onomeneq 4504  0sdom1dom 4510  omsdomnn 4515  domfi 4522  unblem4 4526  unfilem1 4530  unifi 4538  pwfi 4551  supmo 4556  supmax 4569  suppr 4570  supsnALT 4572  inf0 4586  infensuc 4618  r1tr 4634  r1ord 4635  tz9.12lem1 4639  tz9.12lem3 4641  tz9.12 4642  rankon 4651  rankr1lem 4653  rankval3 4661  bndrank 4662  unbndrank 4663  rankr1b 4679  rankval4 4682  rankbnd2 4684  rankxplim 4692  rankxplim3 4694  rankxpsuc 4695  scott0 4697  karden 4706  numth2 4765  numthcor 4766  zorn2lem2 4769  zorn2lem4 4771  zorn2lem5 4772  zorn 4777  brdom7disj 4784  brdom6disj 4785  iundom 4792  oncardval 4799  oncardon 4800  oncardid 4801  oncard 4809  cardne 4810  carden 4811  sucdom 4822  unxpdom2 4825  sucxpdom 4826  cardidm 4829  cardsdomel 4832  carduni 4838  cardmin 4840  cardprc 4841  alephon 4845  alephcard 4847  alephordi 4854  alephgeom 4862  alephprc 4873  alephfplem3 4878  alephfp 4880  cardcf 4891  cfsuc 4895  cdaun 4902  cdadom2 4914  indpi 5014  ltsopq 5055  ltrpq 5065  prub 5078  genpnnp 5088  distrlem4pr 5110  prlem934b 5118  ltapr 5131  addcanpr 5132  suplem2pr 5142  ltsosr 5183  sqgt0sr 5195  mappsrpr 5198  suppsr2 5203  suppsr3 5204  supsrlem1 5205  ltsor 5241  axmulopr 5246  axmulass 5258  axdistr 5259  axcnre 5266  pre-axlttri 5267  pre-axlttrn 5268  addid2t 5309  cnegextlem2 5326  cnegext 5328  0cnALT 5330  addcan 5331  negclt 5348  mulid2t 5397  muladd11t 5402  mul02t 5424  mulm1t 5451  axmulgt0 5486  lttri2t 5493  lttri3t 5494  ltnrt 5511  mnfltt 5524  pnfnltt 5527  mnflet 5530  xrlttri2t 5536  xrlttri3t 5537  xrltnet 5546  ngtmnftt 5548  ne0gt0t 5601  lt0neg2t 5650  le0neg2t 5652  recextlem1 5663  recext 5665  mulcan 5667  mul0or 5671  divassz 5716  divdiv23z 5758  ltp1t 5775  lemul1it 5801  lemul1itOLD 5802  recgt0 5824  ltdiv23 5850  recp1lt1 5857  recrecltt 5858  posex 5864  squeeze0 5880  nnleltp1t 5909  nnsub 5911  nnaddm1clt 5913  avglet 5999  suprubi 6017  suprleubi 6020  xrsupsslem 6031  xrinfmsslem 6032  nn0ge0t 6072  nn0ltp1let 6082  elnn0z 6102  elnnz1 6110  elnn0nn 6126  zltp1let 6136  recnzt 6146  zneo 6155  zneoOLD 6156  zqt 6206  nnrecqt 6222  qbtwnxr 6225  qsqueeze 6226  rpge0t 6233  om2uzuz 6242  om2uzran 6245  uzrdgsuc 6249  seq1m1 6264  seq1rn2 6266  shftfval 6287  shftidt 6300  icounlem 6353  snunioolem 6355  uzind4i 6394  fzelp1 6449  fzshftralt 6462  fseqsupub 6466  seq1seq02t 6483  seqz1 6487  seqzp1 6488  seq0p1 6491  seqzval2t 6493  1expt 6524  0expt 6529  expge0t 6530  expge1t 6532  expwordit 6542  exple1t 6546  expubndt 6547  sqgt0 6566  sqlecant 6580  subsq2t 6582  bernneq 6591  bernneq2 6592  expnbndt 6593  discrlem2 6595  nnesq 6600  sqrlem5 6615  sqrlem6 6616  sqrlem12 6622  sqrlem16 6626  sqrlem17 6627  sqrge0 6640  sqrmsq 6647  crrecz 6680  rimul 6683  replimtOLD 6701  crret 6710  crimt 6712  imret 6718  reim0t 6719  recjt 6761  imcjt 6762  cjreimt 6771  cjreim2t 6772  cj11t 6773  absreimsqt 6799  absreimt 6800  absdivz 6802  absort 6808  absnid 6814  abslt 6818  absle 6819  absltOLD 6820  absleOLD 6821  cjdiv 6834  abs3lem 6846  abs1m 6849  cau5i 6862  cvg3 6868  caubnd 6871  facdivt 6887  faclbnd2 6891  faclbnd3 6892  faclbnd4lem1 6893  faclbnd4lem3 6895  faclbnd4lem4 6896  faclbnd5 6898  bcnp11t 6911  bcnp1nt 6912  bcpasc 6915  bccl2t 6917  sumex 6927  fsum1slem 6954  fsum1s 6955  csbfsumlem 6972  serzsplit 7002  binomlem1 7012  binomlem2 7013  binomlem3 7014  binomlem4 7015  binomlem5 7016  binomlem6 7017  binom1p 7019  clm2 7024  clm4 7026  clm0 7029  clm0nns 7031  climconst 7039  climunii 7043  climreu 7046  climshft 7049  climshft2 7051  iserzshft2 7052  climrecl 7055  climge0 7057  climaddlem2 7059  climaddc2 7063  climmullem1 7064  climmullem2 7065  climmullem3 7066  climmullem4 7067  climmullem7 7070  climsub 7074  clim2serzt 7078  clim2serz 7089  iserzex 7090  climubi 7097  climsup 7099  climcau 7100  caucvglem6 7106  caucvg 7107  caucvg3a 7108  caucvg3lem 7110  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1cmp2 7121  cvgcmp2lem 7124  cvgcmp2clem 7126  isumshft 7147  isumshft2 7148  isumclt 7152  iserzgt0 7154  reccnv 7161  infcvglem1 7164  infcvglem3 7166  expcnvlem2 7171  expcnvlem6 7175  geoser 7177  geolimilem 7178  geolim1i 7181  geoisum 7185  geoisum1 7187  geoisum1c 7188  0.999... 7189  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag2 7202  cncfval 7207  ivthlem1 7224  ivthlem2 7225  ivthlem7 7230  ivthlem7OLD 7239  efcltlem1 7254  dfef2 7257  ef0lem 7260  efclt 7262  efcvg 7264  efcvgfsum 7265  reefcl 7267  erelem1 7269  erelem2 7270  erelem3 7271  efcj 7286  efaddlem1 7288  efaddlem2 7289  efaddlem3 7290  efaddlem5 7292  efaddlem6 7293  efaddlem10 7297  efaddlem11 7298  efaddlem13 7300  efaddlem16 7303  efaddlem17 7304  efaddlem19 7306  efaddlem25 7312  efaddlem26 7313  efaddlem27 7314  efsubt 7321  efnn0valt 7323  eftabs 7325  eftlexOLD 7327  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  absef01tllem 7336  eirrlem2 7339  eirrlem3 7340  eirrlem4 7341  eirrlem5 7342  abspef01tlub 7344  efsep 7345  effsumle 7346  efm1lim 7359  absefm1le 7360  eflegeolem1 7361  eflegeolem2 7362  efcnlem1 7367  reeff1o 7376  sinclt 7381  cosclt 7382  resinvalt 7383  recosvalt 7384  efi4pt 7385  resin4pt 7386  recos4pt 7387  resinclt 7388  recosclt 7389  sinnegt 7392  cosnegt 7393  efivalt 7397  efmivalt 7398  efeult 7399  sin01bndlem1 7417  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos01gt0 7427  sin02gt0 7428  demoivre 7434  demoivreALT 7435  acdc3lem 7436  acdclem 7444  nn0ennn 7447  znnenlem 7451  znnenlemOLD 7452  znnen 7453  unbenlem 7455  ruclem13 7473  ruclem15 7475  ruclem28 7488  ruclem31 7491  infxpidmlem10 7512  infxpidmlem12 7514  infunabs 7516  infcdaabs 7517  infcda 7518  infdif 7519  infdif2 7520  infxp 7523  infmap1 7524  iunctb 7525  unctb 7527  infmap2 7531  alephadd 7532  alephexp1 7534  alephexp2 7536  gch-kn 7537  tgvalt 7566  metgt0 7772  metxplem3 7780  metxp 7786  blfval 7787  bl2in 7795  lpbl 7832  lmfval 7877  caufval 7878  lmbr 7880  lmnn 7887  iscau 7888  lmclim 7914  metelcls 7916  xplm 7925  oprcn 7927  opr1scn 7930  bopcnlem1 7931  bopcnlem4 7934  cncms 7948  bcthlem1 7949  bcthlem7 7955  bcthlem8 7956  bcthlem9 7957  bcthlem10 7958  bcthlem11 7959  bcthlem16 7964  bcthlem18 7966  bcthlem20 7968  bcthlem21 7969  bcthlem22 7970  bcthlem23 7971  bcthlem28 7976  bcthlem33 7981  isgrp2i 8026  issubgi 8074  addinv 8080  ablmul 8083  mulid 8084  ghgrpilem1 8085  ghgrpilem3 8087  ghgrpilem4 8088  ghgrpi 8089  isvc 8152  nvop2 8179  nvvop 8180  nvop 8257  cnnvdemo 8261  imsmetlem 8274  sqcn 8283  nmcnilem 8285  va1cnlem 8292  sm1cnilem 8294  ipfval 8299  ipval2 8304  4ipval2 8305  4ipval3 8309  ipid 8310  ipcl 8312  ipcj 8314  ip1cnilem1 8320  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem4 8323  ip1cnilem5 8324  ip1cnilem6 8325  sspival 8344  lnocoi 8365  nmoubi 8380  nmoub3i 8381  nmounbi 8384  0oo 8394  nmlno0lem 8398  nmlnogt0 8402  nmblolbii 8403  blocnilem 8408  blocni 8409  phop 8421  cnph 8422  ipasslem1 8434  ipasslem2 8435  ipasslem4 8437  ipasslem5 8438  ipasslem9 8442  ipasslem11 8444  siilem1 8455  siii 8457  ipblnfi 8460  ip2eqi 8461  ubthlem4 8476  ubthlem5 8477  ubthlem6 8478  ubthlem7 8479  ubthlem8 8480  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  minveclem5 8493  minveclem9 8497  minveclem10 8498  minveclem14 8502  minveclem16 8504  minveclem18 8506  minveclem19 8507  minveclem20 8508  minveclem21 8509  minveclem22 8510  minveclem25 8513  minveclem26 8514  minveclem27 8515  minveclem28 8516  minveclem29 8517  minveclem30 8518  minveclem31 8519  minveclem35 8523  minveclem36 8524  minveclem37 8525  minveclem38 8526  minveceu 8527  htthlem6 8568  htthlem7 8569  htthlem8 8570  htthlem9 8571  htthlem10 8572  htthlem12 8574  sincolem 8603  sincnlem 8604  pilem1 8609  pilem2 8610  pilem3 8611  sinperlem1 8624  efimpi 8634  sinhalfpip 8635  sinhalfpim 8636  coshalfpip 8637  coshalfpim 8638  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincos6thpi 8647  cosh111lem1 8648  efghgrpilem 8653  efif 8655  efifolem1 8656  efifolem2 8657  efifolem4 8659  efifolem6 8661  efif1lem1 8664  efif1lem4 8667  efielcircOLD 8674  circgrpOLD 8677  efielcirc 8678  shftefif1olem 8680  eff1lem 8682  eff1i 8683  effoi 8684  efper 8686  eflogt 8699  logeft 8701  axhvass 8793  axhvaddid 8795  axhvmulid 8797  axhvmulass 8798  axhvdistr1 8799  axhvdistr2 8800  axhvmul0 8801  axhis2 8804  axhis3 8805  axhcompl 8807  hvsubopr 8824  hvsubclt 8826  hv2negt 8836  hvaddsubvalt 8841  hvsub4t 8845  hvaddsub12t 8846  hvpncant 8847  hvaddsubasst 8849  hvsubdistr1t 8855  hvaddeq0t 8875  hvsubcant 8880  his2subt 8897  hi01t 8901  normnegt 8950  norm3lem 8955  hilabl 8966  hilid 8967  hilnorm 8969  hhcms 9011  hhssnv 9073  hhsscms 9089  projlem6 9130  projlem26 9150  pjthlem2 9158  pjthlem3 9159  pjthlem7 9163  pjthlem8 9164  pjtheu 9173  omlsi 9183  pjcl 9189  pjhcl 9190  ococint 9235  spanvalt 9237  spanclt 9242  shlub 9284  shslub 9296  h1de2ctlem 9417  spanunsn 9442  pjoml6 9472  cm0t 9492  osumlem7 9524  spansncv 9537  pjocin 9583  pjin 9584  pjjs 9585  pjrn 9587  pjv 9590  pjds 9597  pjoi0 9603  mayete3 9613  ho0valt 9616  homulid2t 9666  hosubnegt 9673  hosubdit 9674  honegsubdit 9676  honegsubdi2t 9677  hosub4t 9679  hoaddsubasst 9681  hosubsub4t 9684  eigre 9700  eigpos 9702  nmopsetretHIL 9731  adjvalt 9754  adjt 9796  nmlnop0ALT 9858  lnopeq0 9870  hmopdt 9885  nmbdoplb 9887  nmcopexlem3 9891  nmcopexlem4 9892  nmcoplb 9896  lnopcon 9901  nmbdfnlb 9916  nmcfnexlem3 9920  nmcfnexlem4 9921  nmcfnlb 9925  lnfncon 9928  nlelsh 9931  nlelch 9932  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem7 9944  adjbd1o 9956  nmopadjle 9959  nmopadjlem 9960  nmopco 9966  nmopcoadj 9972  branmfnt 9976  bra11 9979  cnvbravalt 9981  cnvbraclt 9982  cnvbrabrat 9983  bracnvbrat 9984  leoppost 9997  nmopleidt 10010  pjnmop 10013  hmopidmchlem 10016  pjss1co 10029  pjnormss 10034  pjorthco 10035  pjtot 10045  pjadj3t 10053  pjinvar 10057  pjclem4a 10064  pj3lem1 10072  pj3s 10073  pjs14 10076  hst1ht 10092  strlem4 10119  strlem5 10120  hstrlem4 10127  hstrlem5 10128  jplem1 10133  mdslle1 10181  mdslle2 10182  mdslj1 10183  mdslj2 10184  mdsl1 10185  mdsl2 10186  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd2 10194  csmdsym 10198  mdexch 10199  elat2 10204  shatomic 10222  shatomistic 10225  chrelat 10228  chrelat2 10229  cvat 10230  cvbr3 10231  cvexchlem 10232  atoml 10246  atoml2 10247  atord 10248  atcvat2 10251  irredlem4 10257  atcvat3 10260  atcvat4 10261  atabs 10265  mdsymlem1 10267  mdsymlem3 10269  mdsymlem5 10271  mdsymlem6 10272  sumdmdlem 10281  sumdmdlem2 10282  dmdbr5at 10284  cdj1 10294  cdj3lem1 10295  ghomgrpilem2 10320  symggrpi 10340  cayleylem1 10343  cayleylem2 10344  cayleylem3 10345  gelsupvalOLD 10354  uninqs 10378  qusp 10466  efilcp 10481  efilcp2 10486  mslb1 10509  2wsms 10510  eloi 10539  dedalg 10556  catded 10577  hgrablkcard 10646

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain