Theorem mpan 756

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

Syntax hints:   -> wi 3   /\ wa 239

This theorem is referenced by:  mp2an 758  mpanl1 767  mpanl12 770  mp3an1 1025  mp3an12 1028  mp3an13 1029  sbcbii 2339  csbex 2382  csbie2t 2411  csbnestg 2414  csbabg 2421  csbabgOLD 2422  ssdifss 2568  elssuni 3028  difexg 3273  rabexg 3275  abssexg 3305  snex 3307  copsexg 3352  fr2nr 3450  trsuc 3564  oneli 3588  on0eqel 3598  unexb 3608  opeluu 3616  rabxfr 3654  reuhyp 3660  fr3nr 3670  onminsb 3690  onminesb 3691  onintrab 3693  onnminsb 3696  onminex 3699  onuninsuci 3732  limuni3 3747  tfindsg2 3756  dfom2 3762  brrelexi 3840  relsn 3898  xpss2 3903  xpexg 3906  opabid2 3918  brelrn 4002  dmexg 4017  rnexg 4018  resexg 4061  soirri 4125  sotri 4126  dfrel2 4169  coi1 4224  resfunexg 4311  opabex2g 4351  fco 4384  fssres 4393  fabexg 4407  fvopab3 4551  fvimacnv 4589  ffvelrni 4599  rnssopab 4609  fopabco 4616  fopabcos 4617  fvconst2 4633  fo1stres 4847  fo2ndres 4848  elopabi 4870  eloprabi 4871  fparlem1 4892  fparlem2 4893  rdgsucopab 4965  rdglim2 4968  frsucopab 4973  tz7.48lem 4975  tz7.48-1 4976  tz7.48-2 4977  tz7.49 4979  abianfplem 4981  abianfp 4982  ordgt0ge1 5000  oe0m 5013  oa0r 5031  om0r 5032  om1r 5035  oe1m 5037  oawordeulem 5047  oaass 5054  odi 5069  omass 5070  oneo 5071  oen0 5072  oewordi 5077  oewordri 5078  oeoalem 5082  oeoa 5083  oeoelem 5084  oeoe 5085  oaabs 5120  map0 5214  f1oen 5268  ssdomg 5278  snfi 5302  fiprc 5303  undom 5308  xpdom3 5315  mapdom2 5398  pwen 5407  limenpsi 5409  limensuci 5410  php 5417  0sdom1dom 5428  omsdomnn 5433  domfi 5441  isfinite2 5449  unfilem1 5451  supmo 5476  supmax 5489  suppr 5490  supsnALT 5492  ordtypelem2 5495  ordtypelem4 5497  ordtypelem6 5499  ordtypelem7 5500  hartog 5503  inf0 5521  infensuc 5554  r1tr 5574  r1ord 5575  tz9.12lem1 5579  tz9.12lem3 5581  rankr1lem 5593  rankval3 5601  unbndrank 5603  rankr1b 5619  rankval4 5622  rankxplim3 5634  rankxpsuc 5635  scott0 5643  karden 5652  alephon 5672  omsubsdomlem2 5676  elomsubsd 5681  omsubdmss 5682  omsublim 5683  zorn2lem4 5749  zorn2lem5 5750  brdom7disj 5762  brdom6disj 5763  iundom 5770  oncard 5774  ficardom 5775  cardne 5776  carden 5777  sucdom 5790  cardidm 5797  cardsdomel 5800  carduni 5806  cardmin 5808  cardprc 5809  alephcard 5811  alephordi 5818  alephgeom 5826  alephprc 5837  alephfp 5844  cfsuc 5859  cdaun 5866  cdadom2 5880  nnacda 5884  nnaun 5885  indpi 5982  ltsopq 6023  ltrpq 6033  prub 6046  genpnnp 6056  prlem934b 6086  ltapr 6099  addcanpr 6100  suplem2pr 6110  ltsosr 6151  sqgt0sr 6163  mappsrpr 6166  suppsr2 6171  suppsr3 6172  ltsor 6209  axcnre 6235  pre-axlttri 6236  pre-axlttrn 6237  addid2 6278  cnegex 6298  0cnALT 6300  addcaniOLD 6302  negcl 6321  mulid2 6374  muladd11 6380  mul02 6403  mulm1 6434  axmulgt0 6471  lttri2 6478  lttri3 6479  lttri4 6480  ltnr 6496  ltnsym2 6499  pnfnlt 6517  mnfle 6520  xrlttri2 6526  xrlttri3 6527  xrltne 6536  ngtmnft 6538  ne0gt0 6597  lt0neg2 6654  le0neg2 6656  recextlem1 6670  recex 6672  mulcani 6674  mul0ori 6678  divasszi 6724  ltp1 6784  ltmul2i 6810  lemul1a 6814  lemul1aOLD 6815  recgt0i 6839  recp1lt1 6879  ltdivp1i 6885  posexi 6886  squeeze0 6902  nnrecre 6931  nnsubi 6935  avgle 7026  rpge0 7036  rpreccl 7045  rpneg 7047  suprubii 7066  suprleubii 7069  xrsupsslem 7080  xrinfmsslem 7081  nn0ltp1le 7131  elnnz1 7159  elnn0nn 7175  recnz 7198  zneo 7207  zq 7235  nnrecq 7251  qbtwnxr 7255  qsqueeze 7256  icounlem 7376  snunioolem 7378  uzind4i 7418  fzelp1i 7477  fzshftral 7496  fseqsupubi 7500  om2uzuzi 7503  uzrdgsuci 7511  cardfz 7514  seq1m1 7527  shftfval 7550  shftidt 7563  seq1seq02 7581  seqzp1 7586  seq0p1 7589  seqzval2 7591  1exp 7622  0exp 7627  expge0 7628  expge1 7630  expwordi 7643  exple1 7647  sqgt0i 7667  sqlecan 7682  subsq2 7684  bernneq 7693  bernneqOLD 7694  expnbnd 7696  expnlbnd2 7698  discrlem2 7702  nnesqi 7707  nn0opthlem2 7710  sqrlem5 7722  sqrlem6 7723  sqrlem16 7733  sqrge0i 7747  sqrmsqi 7754  crreczi 7786  rimul 7789  recj 7863  absor 7911  absnidi 7918  abslti 7922  abslei 7923  abs1mi 7951  cau5ii 7964  cvg3i 7970  faclbnd2 7993  faclbnd3 7994  faclbnd4lem1 7995  faclbnd4lem3 7997  faclbnd4lem4 7998  bcnp11 8012  bcnp1n 8013  bcpasci 8016  bccl2 8018  fz1fi 8024  hashginv 8026  hashfz1 8027  sumex 8036  fsum1slem 8063  fsum1s 8064  csbfsumlem 8081  serzsplit 8111  binomlem1 8121  binomlem2 8122  binomlem3 8123  binomlem4 8124  binomlem5 8125  binom1pi 8128  clm2i 8133  clm0nnsi 8140  climunii 8153  climreu 8156  climshfti 8159  climshft2i 8161  climrecl 8165  climge0 8167  climaddlem2 8170  climaddc2 8174  climmullem7 8181  climsub 8185  clim2serz 8189  iserzexi 8201  climubii 8208  climsupi 8210  caucvg3lem 8221  serzf0i 8224  ser1cmp2i 8232  isum1clim 8253  isumshfti 8260  isumshft2i 8261  isumcl 8265  iserzgt0 8267  reccnv 8274  expcnvlem2 8284  expcnvlem6 8288  geoseri 8291  geolimilem 8292  geolim1i 8295  geoisum1c 8302  0.999... 8303  cvgratlem1ALT 8304  cvgratlem2ALT 8305  cvgratlem5 8311  fsum0diaglem2 8314  fsum0diag2 8316  ivthlem2 8339  ivthlem7 8344  efcltlem1 8361  dfef2i 8364  reefcli 8374  erelem3 8378  efcji 8393  efaddlem2 8396  efaddlem3 8397  efaddlem5 8399  efaddlem6 8400  efaddlem10 8404  efaddlem11 8405  efaddlem13 8407  efaddlem16 8410  efaddlem17 8411  efaddlem19 8413  efaddlem25 8419  efnn0val 8430  eftabsi 8432  eftlexiOLD 8434  ef1tllem 8438  ef01tllem1 8440  absef01tllem 8444  eirrlem2 8447  eirrlem3 8448  eirrlem4 8449  eirrlem5 8450  abspef01tlubi 8455  efsepi 8456  effsumlei 8457  efm1limi 8471  absefm1lei 8472  eflegeolem1 8473  eflegeolem2 8474  reeff1o 8486  sincl 8491  coscl 8492  sinneg 8502  cosneg 8503  efival 8507  efmival 8508  sin01bndlem1 8528  cos01gt0 8538  sin02gt0 8539  absefib 8545  efieq1re 8546  demoivre 8547  demoivreALT 8548  acdc4lem1 8551  nn0ennn 8561  znnen 8566  unbenlem 8568  ruclem13 8586  ruclem15 8588  ruclem28 8601  ruclem31 8604  infxpidmlem10 8625  infxpidmlem12 8627  infunabs 8629  infcdaabs 8630  infdif2 8633  infxp 8636  infmap1 8637  iunctb 8639  infmap2 8645  alephexp2 8650  tgval 8681  indistop 8713  metxp 8906  blfval 8907  bl2in 8915  lpbl 8952  lmfval 8998  caufval 8999  lmnn 9008  lmclim 9036  xplm 9048  oprcn 9050  opr1scn 9053  bopcnlem1 9054  cncms 9071  bcthlem1 9072  bcthlem7 9078  bcthlem8 9079  bcthlem9 9080  bcthlem10 9081  bcthlem11 9082  bcthlem16 9087  bcthlem21 9092  bcthlem33 9104  issubgi 9226  addinv 9231  ablmul 9234  mulid 9235  ghgrpilem1 9236  ghgrpilem3 9238  ghgrpilem4 9239  drngi 9288  nvop2 9354  nvop 9432  cnnvdemo 9437  imsmetlem 9450  vacnlem2 9463  vacnlem3 9464  sqcn 9469  nmcnilem 9471  va1cnlem 9479  sm1cnilem 9481  ipfval 9486  ipval2 9491  4ipval2 9492  4ipval3 9496  ipid 9497  ipcl 9499  ipcj 9501  ip1cnilem1 9507  ip1cnilem2 9508  ip1cnilem3 9509  ip1cnilem4 9510  ip1cnilem5 9511  ip1cnilem6 9512  sspival 9531  lnocoi 9552  nmoubi 9569  nmoub3i 9570  nmounbi 9573  0oo 9584  nmlno0lem 9588  nmlnogt0 9592  nmblolbii 9594  blocnilem 9599  blocni 9600  phop 9613  cnph 9614  ipasslem1 9626  ipasslem2 9627  ipasslem4 9629  ipasslem5 9630  ipasslem9 9634  ipasslem11 9636  siilem1 9647  siii 9649  ipblnfi 9652  ip2eqi 9653  ubthlem4 9670  ubthlem6 9672  ubthlem7 9673  ubthlem8 9674  ubthlem9 9675  ubthlem10 9676  ubthlem11 9677  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  minveclem5 9689  minveclem9 9693  minveclem10 9694  minveclem14 9698  minveclem16 9700  minveclem18 9702  minveclem19 9703  minveclem20 9704  minveclem21 9705  minveclem22 9706  minveclem25 9709  minveclem26 9710  minveclem27 9711  minveclem28 9712  minveclem29 9713  minveclem30 9714  minveclem31 9715  minveclem35 9719  minveclem36 9720  minveclem37 9721  minveclem38 9722  minveceu 9723  htthlem6 9767  htthlem7 9768  htthlem8 9769  htthlem9 9770  htthlem10 9771  htthlem12 9773  sincolem 9809  sincnlem 9810  pilem1 9815  pilem2 9816  pilem3 9817  sinperlem1 9830  efimpi 9842  sinhalfpip 9843  sinhalfpim 9844  coshalfpip 9845  coshalfpim 9846  sincosq1sgn 9848  sincosq2sgn 9849  sincosq3sgn 9850  sincosq4sgn 9851  sinq12gt0t 9852  sincos6thpi 9856  sinkpi 9858  coskpi 9859  sineq0re 9862  cosh111lem1 9863  efghgrpilem 9868  efif 9870  efifolem1 9871  efifolem2 9872  efifolem4 9874  efifolem6 9876  efif1lem1 9879  efif1lem4 9882  efielcirc 9888  shftefif1olem 9890  eff1lem 9892  eff1i 9893  effoi 9894  efper 9896  eflog 9909  logef 9911  twpar2 9942  oprabopabf 9951  setwoe 9964  fixp 9972  symggrpi 9998  fiuni 10012  tx1cn 10015  tx2cn 10016  fgfil 10082  extbas1 10083  hausfillim 10095  fintopcomp 10125  ismnd2 10184  ringidmlem 10201  axhvass 10278  axhvaddid 10280  axhvmulid 10282  axhvmulass 10283  axhvdistr1 10284  axhvdistr2 10285  axhvmul0 10286  axhis2 10289  axhis3 10290  axhcompl 10292  hvsubopr 10309  hvsubcl 10311  hv2neg 10321  hvaddsubval 10326  hvsub4 10330  hvaddsub12 10331  hvpncan 10332  hvaddsubass 10334  hvsubdistr1 10340  hvaddeq0 10360  hvsubcan 10366  his2sub 10383  hi01 10387  normneg 10436  norm3lem 10441  hilabl 10452  hilid 10453  hilnormi 10455  hhcms 10497  hhssnv 10559  hhsscms 10575  projlem6 10616  projlem26 10636  projlemHIL 10643  pjthlem2 10645  pjthlem3 10646  pjthlem7 10650  pjthlem8 10651  pjtheui 10660  omlsii 10670  pjcli 10676  pjhcli 10677  ococin 10722  spanval 10724  spancl 10729  shlubi 10771  shslubi 10783  h1de2ctlem 10903  spanunsni 10927  pjoml6i 10957  cm0 10977  osumlem7 11011  spansncvi 11024  pjocini 11070  pjini 11071  pjjsi 11072  pjrni 11074  pjvi 11077  pjdsi 11084  pjoi0i 11090  mayete3i 11100  mayete3OLDi 11101  ho0val 11105  homulid2 11155  hosubneg 11162  hosubdi 11163  honegsubdi 11165  honegsubdi2 11166  hosub4 11168  hoaddsubass 11170  hosubsub4 11173  eigrei 11189  eigposi 11191  eigorthi 11192  nmopsetretHIL 11220  adjval 11243  adj1 11286  nmlnop0iALT 11349  lnopeq0i 11361  hmopd 11376  nmbdoplbi 11378  nmcopexlem3 11382  nmcopexlem4 11383  nmcoplbi 11387  lnopconi 11392  nmbdfnlbi 11407  nmcfnexlem3 11411  nmcfnexlem4 11412  nmcfnlbi 11416  lnfnconi 11419  nlelshi 11422  nlelchi 11423  riesz3i 11424  cnlnadjlem2 11430  cnlnadjlem7 11435  adjbd1o 11447  nmopadjlei 11450  nmopadjlem 11451  nmopcoi 11457  nmopcoadji 11463  branmfn 11467  branmfnOLD 11468  bra11 11471  cnvbraval 11473  cnvbracl 11474  cnvbrabra 11475  bracnvbra 11476  leoppos 11489  nmopleid 11502  opsqrlem1 11503  opsqrlem3 11505  opsqrlem6 11508  pjnmopi 11511  hmopidmchlem 11514  pjss1coi 11527  pjnormssi 11532  pjorthcoi 11533  pjtoi 11543  pjadj3 11552  pjinvari 11556  pjclem4a 11563  pj3lem1 11571  pj3si 11572  pjs14i 11575  hst1h 11591  strlem4 11618  strlem5 11619  hstrlem4 11626  hstrlem5 11627  jplem1 11632  mdslle1i 11681  mdslle2i 11682  mdslj1i 11683  mdslj2i 11684  mdsl1i 11685  mdsl2i 11686  mdslmd1lem1 11689  mdslmd1lem2 11690  mdslmd2i 11694  csmdsymi 11698  mdexchi 11699  elat2 11704  shatomici 11722  shatomistici 11725  chrelati 11728  chrelat2i 11729  cvati 11730  cvbr3i 11731  cvexchlem 11732  atomli 11746  atoml2i 11747  atordi 11748  atcvat2i 11751  irredlem4 11757  atcvat3i 11760  atcvat4i 11761  atabsi 11765  mdsymlem1 11767  mdsymlem3 11769  mdsymlem5 11771  mdsymlem6 11772  sumdmdlem 11782  sumdmdlem2 11783  dmdbr5ati 11786  cdj1i 11797  cdj3lem1 11798  bnj1119 12721  bnj157 12992  bnj522 13053  bnj535 13057  bnj546 13064  elnn00nn 13394  fz1n 13399  zmodid2 13406  zmodfz 13407  fseq1cl 13411  ghomgrpilem2 13421  cayleylem1 13433  cayleylem2 13434  cayleylem3 13435  0dvds 13467  dvdslelem 13484  divalglem0 13488  divalglem2 13490  divalglem4 13491  divalglem5 13492  divalglem6 13493  divalglem9 13496  gcdcllem1 13510  gcd0id 13521  gcdid0 13522  nn0gcdid0 13523  algcvg 13536  algcvgblem 13537  mulgcdlem2 13549  mulgcdlem7 13554  1idssfct 13562  zgt1b2 13564  isprm2lem 13566  isprm3 13568  coprm 13574  elres 13618  elsnres 13619  dfon2lem3 13642  dfon2lem7 13646  predep 13694  wfii 13708  trclss 13727  frindi 13732  poxp 13741  soxp 13742  frxp 13743  poseq 13746  soseq 13747  wfrlem10 13758  wfrlem16 13764  sltirr 13798  slttr 13799  slttri 13801  bdayelon 13807  axdenselem4 13812  nocvxminlem 13818  nocvxmin 13819  axfelem0 13820  axfelem1 13821  axfelem10 13830  dfoprab4spop 14067  uninqs 14068  eloi 14130  set2elt 14138  repcpwti 14229  prl 14238  preoref22 14296  ubos2 14320  supdef 14326  mxlelt2 14328  mnlelt2 14330  defselem 14336  ranncnt 14349  istoset2 14353  tostos 14363  fprod1slem 14400  fprod1s 14401  fincmpzer 14434  symgfo 14453  fprodneg 14464  sallnei 14594  top2usne 14618  subtopsin2 14626  qusp 14627  efilcp 14636  efilcp2 14640  limfillem2 14653  bwt2 14674  topgrpi 14686  trhom 14697  tpgprop2 14701  altretop 14707  cntrsetlem 14709  mslb1 14717  2wsms 14718  dedalg 14772  catded 14793  issubcat 14875  tarsuc2 14927  fnctartar 14966  fnctartar2 14967  elfiun 15051  ordtypelem2OLD 15058  ordtypelem4OLD 15060  ordtypelem6OLD 15062  ordtypelem7OLD 15063  hartogOLD 15066  omsubsdomlem2OLD 15071  elomsubsdOLD 15076  omsubdmssOLD 15077  omsublimOLD 15078  neiin 15100  alexsub 15123  reconnlem1 15128  reconnlem2 15129  reconn 15133  ivthALT 15136  2ndcctbss 15160  fnessref 15185  refssfne 15186  neibastop2lem3 15203  neibastop2lem4 15204  topjoin 15209  isufil2 15247  filssufil 15253  ufileulem 15254  ufileu 15255  filufint 15256  ufilen 15261  flimcls 15270  fmfnfmlem1 15276  fmfnfmlem4 15279  fmfnfm 15280  fclsfnflim 15296  flimfnfcls 15297  fcluscomplem 15302  tailf 15315  tailmap 15318  filnetlem4 15325  filnetlem5 15326  filnet 15327  abrexdom 15421  fimax 15428  indexfi 15437  inficl 15439  fz10 15470  sdc 15493  incsequz2 15498  fsumltisumi 15505  fsumlt1 15513  stioo 15527  mettrifi2 15530  geomcau 15531  caures 15534  iirev 15553  iihalf1 15554  iihalf2 15555  lincmb01icc 15561  oprpiece1res2 15563  piececn 15576  txmet 15607  isbnd3 15623  heiborlem10 15646  heiborlem11 15647  heiborlem13 15649  heiborlem15 15651  heiborlem16 15652  heiborlem23 15659  heiborlem28 15664  heiborlem32 15668  heiborlem35 15671  heiborlem41 15677  bfplem7 15686  phtpyid 15731  phtpycom 15732  phtpycolem2 15734  phtpycolem4 15736  phtpyco 15738  reparpht 15747  pcoval2 15757  pcohtpylem2 15763  pcohtpylem3 15764  pcohtpy 15765  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  isdivrng1 15791  iscring2 15828  hgrablkcard 15978  smores 16128  smoge 16136

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 163  df-an 241

Copyright terms: Public domain