Theorem mpan 699

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 371	. 2 |- (ph -> (ps -> ch))
4	1, 3	ax-mp 7	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  mp2an 701  mpanl1 710  mpanl12 712  mp3an1 909  mp3an12 912  mp3an13 913  sbcbii 2026  sbcel12g 2062  sbceqdig 2063  csbie2t 2085  csbnestg 2088  csbabg 2095  ssdifss 2220  elssuni 2593  difexg 2796  rabexg 2798  fr2nr 2955  oneli 3077  on0eqel 3087  unexb 3096  difex2 3101  opeluu 3103  uniexb 3130  fr3nr 3138  onminsb 3155  onminesb 3156  onintrab 3158  onnminsb 3161  onminex 3164  onuninsuci 3194  limuni3 3206  tfindsg2 3214  dfom2 3220  brrelexi 3291  relsn 3343  xpexg 3348  opabid2 3360  brelrn 3431  dmexg 3445  rnexg 3446  resiexg 3486  imaexg 3508  soirri 3534  sotri 3535  dfrel2 3569  coi1 3614  cnvexg 3624  coexg 3629  resfunexg 3685  cofunexg 3686  opabex2g 3717  fssxp 3744  fssres 3750  fcoi1 3752  fcoi2 3753  fabexg 3760  f1oabexg 3808  fvopab3 3888  fvimacnv 3919  ffvelrni 3929  rnssopab 3939  fopabco 3946  fopabcos 3947  fvconst2 3960  oprabex2g 4080  oprabval 4083  fo1stres 4156  fo2ndres 4157  1stcof 4160  elopabi 4179  eloprabi 4180  fparlem1 4199  fparlem2 4200  rdgsucopab 4247  rdglim2 4250  frsucopab 4255  tz7.48lem 4256  tz7.48-1 4257  tz7.48-2 4258  tz7.49 4260  tz7.49c 4261  abianfplem 4262  abianfp 4263  ordgt0ge1 4280  oe0m 4293  oa0r 4309  om0r 4310  om1r 4313  oe1m 4315  oawordeulem 4324  oaass 4331  odi 4346  omass 4347  oneo 4348  oen0 4349  oewordi 4354  oewordri 4355  oeoalem 4359  oeoa 4360  oeoelem 4361  oeoe 4362  oaabslem 4391  oaabs 4392  mapex 4469  map0 4485  ixpexg 4499  f1oen 4539  ssdomg 4549  snfi 4573  fiprc 4574  undom 4579  xpdom3 4586  mapdom2 4641  pwen 4650  limenpsi 4652  limensuci 4653  php 4660  onomeneq 4665  0sdom1dom 4671  omsdomnn 4676  domfi 4684  unblem4 4689  isfinite2 4692  unfilem1 4694  pwfi 4714  supmo 4719  supmax 4732  suppr 4733  supsnALT 4735  inf0 4751  infensuc 4784  r1tr 4800  r1ord 4801  tz9.12lem1 4805  tz9.12lem3 4807  tz9.12 4808  rankon 4817  rankr1lem 4819  rankval3 4827  bndrank 4828  unbndrank 4829  rankr1b 4845  rankval4 4848  rankbnd2 4850  rankxplim 4858  rankxplim3 4860  rankxpsuc 4861  scott0 4863  karden 4872  numth2 4931  numthcor 4932  zorn2lem2 4935  zorn2lem4 4937  zorn2lem5 4938  zorn 4943  brdom7disj 4950  brdom6disj 4951  iundom 4958  oncardval 4965  oncardon 4966  oncardid 4967  oncard 4976  ficardom 4977  cardne 4978  carden 4979  sucdom 4992  unxpdom2 4995  sucxpdom 4996  cardidm 4999  cardsdomel 5002  carduni 5008  cardmin 5010  cardprc 5011  alephon 5015  alephcard 5017  alephordi 5024  alephgeom 5032  alephprc 5043  alephfplem3 5048  alephfp 5050  cardcf 5061  cfsuc 5065  cdaun 5072  cdadom2 5086  nnacda 5090  nnaun 5091  indpi 5188  ltsopq 5229  ltrpq 5239  prub 5252  genpnnp 5262  distrlem4pr 5284  prlem934b 5292  ltapr 5305  addcanpr 5306  suplem2pr 5316  ltsosr 5357  sqgt0sr 5369  mappsrpr 5372  suppsr2 5377  suppsr3 5378  supsrlem1 5379  ltsor 5415  axmulopr 5420  axmulass 5432  axdistr 5433  axcnre 5440  pre-axlttri 5441  pre-axlttrn 5442  addid2 5483  cnegexlem2 5500  cnegex 5502  0cnALT 5504  addcani 5505  negcl 5522  mulid2 5571  muladd11 5576  mul02 5598  mulm1 5625  axmulgt0 5660  lttri2 5667  lttri3 5668  ltnr 5684  mnflt 5697  pnfnlt 5700  mnfle 5703  xrlttri2 5709  xrlttri3 5710  xrltne 5719  ngtmnft 5721  ne0gt0 5773  lt0neg2 5823  le0neg2 5825  recextlem1 5838  recex 5840  mulcani 5842  mul0ori 5846  divasszi 5891  ltp1 5951  ltmul2i 5977  lemul1a 5981  lemul1aOLD 5982  recgt0i 6006  recp1lt1 6046  recreclt 6047  ltdivp1i 6052  posexi 6053  squeeze0 6069  nnrecre 6098  nnleltp1 6100  nnsubi 6102  nnaddm1cl 6104  avgle 6190  rpge0 6200  rpreccl 6209  rpneg 6211  suprubii 6230  suprleubii 6233  xrsupsslem 6244  xrinfmsslem 6245  nn0ge0 6285  nn0ltp1le 6295  elnn0z 6315  elnnz1 6323  elnn0nn 6339  zltp1le 6349  recnz 6362  zneo 6371  zq 6399  nnrecq 6415  qbtwnxr 6419  qsqueeze 6420  modid 6471  icounlem 6539  snunioolem 6541  uzind4i 6581  fzelp1i 6640  fzshftral 6653  fseqsupubi 6657  om2uzuzi 6660  om2uzrani 6663  uzrdgsuci 6668  cardfz 6671  seq1m1 6684  seq1rn2 6686  shftfval 6707  shftidt 6720  seq1seq02 6738  seqz1 6742  seqzp1 6743  seq0p1 6746  seqzval2 6748  1exp 6779  0exp 6784  expge0 6785  expge1 6787  expwordi 6800  exple1 6804  expubnd 6805  sqgt0i 6824  sqlecan 6838  subsq2 6840  bernneq 6849  bernneqOLD 6850  bernneq2 6851  expnbnd 6852  expnlbnd2 6854  discrlem2 6858  nnesqi 6863  sqrlem5 6878  sqrlem6 6879  sqrlem12 6885  sqrlem16 6889  sqrlem17 6890  sqrge0i 6903  sqrmsqi 6910  crreczi 6942  rimul 6945  crre 6970  crim 6971  imre 6974  reim0 6975  mulre 6978  recj 7019  imcj 7020  cjreim 7029  cjreim2 7030  cj11OLD 7032  absreimsq 7058  absreim 7059  absdivzi 7061  absor 7067  absnidi 7074  abslti 7078  abslei 7079  cjdivi 7091  abs3lemi 7104  abs1mi 7107  cau5ii 7120  cvg3i 7126  caubndi 7129  facdiv 7145  faclbnd2 7149  faclbnd3 7150  faclbnd4lem1 7151  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd5 7156  bcnp11 7168  bcnp1n 7169  bcpasci 7172  bccl2 7174  sumex 7184  fsum1slem 7211  fsum1s 7212  csbfsumlem 7229  serzsplit 7259  binomlem1 7269  binomlem2 7270  binomlem3 7271  binomlem4 7272  binomlem5 7273  binomlem6 7274  binom1pi 7276  clm2i 7281  clm4i 7283  clm0i 7286  clm0nnsi 7288  climconsti 7297  climunii 7301  climreu 7304  climshfti 7307  climshft2i 7309  iserzshft2i 7310  climrecl 7313  climge0 7315  climaddlem2 7318  climaddc2 7322  climmullem1 7323  climmullem2 7324  climmullem3 7325  climmullem4 7326  climmullem7 7329  climsub 7333  clim2serz 7337  clim2serzi 7348  iserzexi 7349  climubii 7356  climsupi 7358  climcaui 7359  caucvglem6 7365  caucvgi 7366  caucvg3ai 7367  caucvg3lem 7369  caucvg3 7371  serzf0i 7372  ser1cmp2i 7380  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  isum1clim 7401  isumshfti 7408  isumshft2i 7409  isumcl 7413  iserzgt0 7415  reccnv 7422  infcvglem1 7425  infcvglem3 7427  expcnvlem2 7432  expcnvlem6 7436  geoseri 7439  geolimilem 7440  geolim1i 7443  geoisum 7447  geoisum1 7449  geoisum1c 7450  0.999... 7451  cvgratlem1ALT 7452  cvgratlem2ALT 7453  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag2 7464  cncfval 7469  ivthlem1 7486  ivthlem2 7487  ivthlem7 7492  efcltlem1 7509  dfef2i 7512  ef0lem 7515  efcl 7517  efcvg 7519  efcvgfsum 7520  reefcli 7522  erelem1 7524  erelem2 7525  erelem3 7526  efcji 7541  efaddlem1 7543  efaddlem2 7544  efaddlem3 7545  efaddlem5 7547  efaddlem6 7548  efaddlem10 7552  efaddlem11 7553  efaddlem13 7555  efaddlem16 7558  efaddlem17 7559  efaddlem19 7561  efaddlem25 7567  efaddlem26 7568  efaddlem27 7569  efnn0val 7578  eftabsi 7580  eftlexiOLD 7582  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  absef01tllem 7592  eirrlem2 7595  eirrlem3 7596  eirrlem4 7597  eirrlem5 7598  abspef01tlubi 7603  efsepi 7604  effsumlei 7605  efm1limi 7619  absefm1lei 7620  eflegeolem1 7621  eflegeolem2 7622  efcnlem1 7627  reeff1o 7634  sincl 7639  coscl 7640  resinval 7641  recosval 7642  efi4p 7643  resin4p 7644  recos4p 7645  resincl 7646  recoscl 7647  sinneg 7650  cosneg 7651  efival 7655  efmival 7656  efeul 7657  cos2tsin 7672  sin01bndlem1 7676  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  cos01gt0 7686  sin02gt0 7687  absefib 7693  efieq1re 7694  demoivre 7695  demoivreALT 7696  acdc3lem 7697  acdc4lem1 7699  acdclem 7706  nn0ennn 7709  znnenlem 7713  znnen 7714  unbenlem 7716  ruclem13 7734  ruclem15 7736  ruclem28 7749  ruclem31 7752  infxpidmlem10 7773  infxpidmlem12 7775  infunabs 7777  infcdaabs 7778  infcda 7779  infdif 7780  infdif2 7781  infxp 7784  infmap1 7785  infpss 7786  iunctb 7787  unctb 7789  infmap2 7793  alephadd 7794  alephexp1 7796  alephexp2 7798  gch-kn 7799  tgval 7828  indistop 7860  metgt0 8030  metxplem3 8038  metxp 8044  blfval 8045  bl2in 8053  lpbl 8090  lmfval 8136  caufval 8137  lmbr 8139  lmnn 8146  iscau 8147  lmclim 8174  metelcls 8176  xplm 8186  oprcn 8188  opr1scn 8191  bopcnlem1 8192  bopcnlem4 8195  cncms 8209  bcthlem1 8210  bcthlem7 8216  bcthlem8 8217  bcthlem9 8218  bcthlem10 8219  bcthlem11 8220  bcthlem16 8225  bcthlem18 8227  bcthlem20 8229  bcthlem21 8230  bcthlem22 8231  bcthlem23 8232  bcthlem28 8237  bcthlem33 8242  isgrp2i 8293  issubgi 8364  addinv 8369  ablmul 8372  mulid 8373  ghgrpilem1 8374  ghgrpilem3 8376  ghgrpilem4 8377  ghgrpi 8378  drngi 8408  isvc 8447  nvop2 8474  nvvop 8475  nvop 8552  cnnvdemo 8557  imsmetlem 8570  vacnlem2 8583  vacnlem3 8584  sqcn 8589  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  ipfval 8606  ipval2 8611  4ipval2 8612  4ipval3 8616  ipid 8617  ipcl 8619  ipcj 8621  ip1cnilem1 8627  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem4 8630  ip1cnilem5 8631  ip1cnilem6 8632  sspival 8651  lnocoi 8672  nmoubi 8689  nmoub3i 8690  nmounbi 8693  0oo 8704  nmlno0lem 8708  nmlnogt0 8712  nmblolbii 8714  blocnilem 8719  blocni 8720  phop 8733  cnph 8734  ipasslem1 8746  ipasslem2 8747  ipasslem4 8749  ipasslem5 8750  ipasslem9 8754  ipasslem11 8756  siilem1 8767  siii 8769  ipblnfi 8772  ip2eqi 8773  ubthlem4 8790  ubthlem5 8791  ubthlem6 8792  ubthlem7 8793  ubthlem8 8794  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  minveclem5 8809  minveclem9 8813  minveclem10 8814  minveclem14 8818  minveclem16 8820  minveclem18 8822  minveclem19 8823  minveclem20 8824  minveclem21 8825  minveclem22 8826  minveclem25 8829  minveclem26 8830  minveclem27 8831  minveclem28 8832  minveclem29 8833  minveclem30 8834  minveclem31 8835  minveclem35 8839  minveclem36 8840  minveclem37 8841  minveclem38 8842  minveceu 8843  htthlem6 8887  htthlem7 8888  htthlem8 8889  htthlem9 8890  htthlem10 8891  htthlem12 8893  sincolem 8932  sincnlem 8933  pilem1 8938  pilem2 8939  pilem3 8940  sinperlem1 8953  efimpi 8965  sinhalfpip 8966  sinhalfpim 8967  coshalfpip 8968  coshalfpim 8969  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  sinq12gt0t 8975  sincos6thpi 8979  sinkpi 8981  coskpi 8982  sineq0re 8985  cosh111lem1 8986  efghgrpilem 8991  efif 8993  efifolem1 8994  efifolem2 8995  efifolem4 8997  efifolem6 8999  efif1lem1 9002  efif1lem4 9005  efielcirc 9011  shftefif1olem 9013  eff1lem 9015  eff1i 9016  effoi 9017  efper 9019  eflog 9032  logef 9034  axhvass 9129  axhvaddid 9131  axhvmulid 9133  axhvmulass 9134  axhvdistr1 9135  axhvdistr2 9136  axhvmul0 9137  axhis2 9140  axhis3 9141  axhcompl 9143  hvsubopr 9160  hvsubcl 9162  hv2neg 9172  hvaddsubval 9177  hvsub4 9181  hvaddsub12 9182  hvpncan 9183  hvaddsubass 9185  hvsubdistr1 9191  hvaddeq0 9211  hvsubcan 9217  his2sub 9234  hi01 9238  normneg 9287  norm3lem 9292  hilabl 9303  hilid 9304  hilnormi 9306  hhcms 9348  hhssnv 9410  hhsscms 9426  projlem6 9467  projlem26 9487  projlemHIL 9494  pjthlem2 9496  pjthlem3 9497  pjthlem7 9501  pjthlem8 9502  pjtheui 9511  omlsii 9521  pjcli 9527  pjhcli 9528  ococin 9573  spanval 9575  spancl 9580  shlubi 9622  shslubi 9634  h1de2ctlem 9754  spanunsni 9778  pjoml6i 9808  cm0 9828  osumlem7 9862  spansncvi 9875  pjocini 9921  pjini 9922  pjjsi 9923  pjrni 9925  pjvi 9928  pjdsi 9935  pjoi0i 9941  mayete3i 9951  mayete3OLDi 9952  ho0val 9956  homulid2 10006  hosubneg 10013  hosubdi 10014  honegsubdi 10016  honegsubdi2 10017  hosub4 10019  hoaddsubass 10021  hosubsub4 10024  eigrei 10040  eigposi 10042  eigorthi 10043  nmopsetretHIL 10071  adjval 10094  adj1 10137  nmlnop0iALT 10199  lnopeq0i 10211  hmopd 10226  nmbdoplbi 10228  nmcopexlem3 10232  nmcopexlem4 10233  nmcoplbi 10237  lnopconi 10242  nmbdfnlbi 10257  nmcfnexlem3 10261  nmcfnexlem4 10262  nmcfnlbi 10266  lnfnconi 10269  nlelshi 10272  nlelchi 10273  riesz3i 10274  cnlnadjlem2 10280  cnlnadjlem7 10285  adjbd1o 10297  nmopadjlei 10300  nmopadjlem 10301  nmopcoi 10307  nmopcoadji 10313  branmfn 10317  branmfnOLD 10318  bra11 10321  cnvbraval 10323  cnvbracl 10324  cnvbrabra 10325  bracnvbra 10326  leoppos 10339  nmopleid 10352  pjnmopi 10355  hmopidmchlem 10358  pjss1coi 10371  pjnormssi 10376  pjorthcoi 10377  pjtoi 10387  pjadj3 10396  pjinvari 10400  pjclem4a 10407  pj3lem1 10415  pj3si 10416  pjs14i 10419  hst1h 10435  strlem4 10462  strlem5 10463  hstrlem4 10470  hstrlem5 10471  jplem1 10476  mdslle1i 10525  mdslle2i 10526  mdslj1i 10527  mdslj2i 10528  mdsl1i 10529  mdsl2i 10530  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd2i 10538  csmdsymi 10542  mdexchi 10543  elat2 10548  shatomici 10566  shatomistici 10569  chrelati 10572  chrelat2i 10573  cvati 10574  cvbr3i 10575  cvexchlem 10576  atomli 10591  atoml2i 10592  atordi 10593  atcvat2i 10596  irredlem4 10602  atcvat3i 10605  atcvat4i 10606  atabsi 10610  mdsymlem1 10612  mdsymlem3 10614  mdsymlem5 10616  mdsymlem6 10617  sumdmdlem 10627  sumdmdlem2 10628  dmdbr5ati 10631  cdj1i 10642  cdj3lem1 10643  ghomgrpilem2 10671  symggrpi 10691  cayleylem1 10694  cayleylem2 10695  cayleylem3 10696  uninqs 10730  twpar2 10773  eloi 10817  set2elt 10827  setwoe 10828  ranncnt 10873  tostos 10883  ismnd2 10928  uridm 10956  sallnei 11016  top2usne 11051  subtopsin2 11067  qusp 11068  efilcp 11083  efilcp2 11087  limfillem2 11102  fintopcomp 11115  bwt2 11123  altretop 11144  mslb1 11152  2wsms 11153  dedalg 11197  catded 11218  issubcat 11299  fiuni 11420  elfiun 11421  ordtypelem2 11428  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  omsubsdomlem2 11441  elomsubsd 11446  omsubdmss 11447  omsublim 11448  neiin 11470  alexsub 11500  reconnlem1 11507  reconnlem2 11508  reconn 11512  ivthALT 11515  2ndcctbss 11539  fnessref 11564  refssfne 11565  neibastop2lem3 11582  neibastop2lem4 11583  topjoin 11588  fgfil 11638  extbas1 11641  isufil2 11650  filssufil 11656  ufileulem 11657  ufileu 11658  filufint 11659  ufilen 11664  flimcls 11684  hausfillim 11685  fmfnfmlem1 11700  fmfnfmlem4 11703  fmfnfm 11704  fclsfnflim 11726  flimfnfcls 11727  fcluscomplem 11732  tailf 11756  tailmap 11759  filnetlem4 11766  filnetlem5 11767  filnet 11768  oprabopabf 11807  abrexdom 11826  fimax 11837  fixp 11840  indexf 11847  inficl 11849  sdc 11877  incsequz2 11880  fsumltisumi 11886  fsumlt1 11894  stioo 11910  mettrifi2 11913  geomcau 11914  caures 11917  iirev 11935  iihalf1 11936  iihalf2 11937  lincmb01icc 11943  piececn 11955  tx1cn 11976  tx2cn 11977  isbnd3 11997  heiborlem10 12020  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem16 12026  heiborlem23 12033  heiborlem28 12038  heiborlem32 12042  heiborlem35 12045  heiborlem41 12051  bfplem7 12060  phtpyid 12091  phtpycom 12092  phtpycolem2 12094  phtpycolem4 12096  phtpyco 12098  hgrablkcard 12200

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 145  df-an 223

Copyright terms: Public domain