Theorem mpan2 760

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpan2.1	|- ps
mpan2.2	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mpan2	|- (ph -> ch)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. 2 |- ps
2		mpan2.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	ex 402	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpi 55	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpanl2 771  mpanl2OLD 772  mpanr2 776  mpanr12 778  mp3an3 1180  mp3an23 1183  euor2OLD 1840  eueq2 2429  eueq3 2430  sbccomg 2526  nnullss 3515  ord0eln0 3717  eldifpw 3854  ordeleqon 3866  ordsson 3867  ordssonOLD 3868  ssnlim 3970  opelxp 4036  xpss1 4091  reldm0 4176  ssres2OLD 4241  resdm 4249  resid 4258  eliniseg 4294  ssrnres 4354  coi2 4414  relrelss 4417  funpr 4467  funcnvres 4487  funimaex 4496  isarep1OLD 4498  fnresin1 4527  fnresin2 4528  dffn2OLD 4564  funssxp 4577  funbrfv 4709  ssimaex 4729  dmfco 4735  fvco 4736  fvopab3 4740  fvopab3ig 4741  fvopab4 4743  fvopab4sf 4745  fvopabn 4749  eufnfv 4771  fvimacnvALT 4782  dff3 4790  rnssopab 4798  fopabco 4805  fsn 4807  fsn2 4809  fopabsnOLD 4816  f1owe 4882  oprabvalig 4953  oprabval2gf 4955  fvmpt 5015  1stval 5022  2ndval 5023  eqop 5044  2ndconst 5071  curry1 5075  tfr3 5134  abianfplem 5170  oa0 5200  om0 5201  oa1suc 5209  om1 5223  oe1 5225  oe1m 5226  oarec 5244  omass 5259  oeoalem 5271  oeoelem 5273  nnmsucr 5295  nneob 5312  ecelqsi 5350  pw2en 5505  ac6sfilem2 5507  ac6sfi 5509  sbthlem7 5516  mapdom1 5586  mapdom2 5588  mapxpen 5589  xpmapenlem2 5591  xpmapenlem4 5593  xpmapenlem5 5594  mapunen 5596  phplem4 5605  infn0 5626  unblem1 5633  unblem2 5634  unblem3 5635  unblem4 5636  isfinite2 5639  unfilem1 5641  unfilem2 5642  unfi 5644  unifi 5648  fiint 5650  fodomfi 5656  pwfilem 5660  pm54.43 5662  inf0 5712  infensuc 5745  trcl 5752  r1suc 5763  rankr1lem 5784  ssrankr1 5787  rankr1a 5788  rankxplim3 5825  scott0 5847  omsubsuc2 5878  omsublim 5887  ac5b 5915  ac6lem 5916  brdom3 5963  brdom5 5964  brdom4 5965  iundom 5974  cardval 5975  carden 5981  cardeq0 5982  card1 5983  unsnen 5985  unxpdomlem 5995  unxpdom2 5997  sucxpdom 5998  alephsuc 6014  alephnbtwn2 6017  alephsucdom 6028  alephle 6032  cardaleph 6033  iscard3 6036  alephfplem2 6045  cflem 6053  cflecard 6060  cfeq0 6062  cdaval 6067  cdadom1 6083  cdadom2 6084  cdainf 6087  nnacda 6088  mulidpi 6166  nlt1pi 6185  indpi 6186  1idpr 6285  prlem934a 6289  prlem934b 6290  0idsr 6358  1idsr 6359  00sr 6360  negexsr 6363  recexsrlem 6364  sqgt0sr 6367  map2psrpr 6372  supsrlem1 6377  supsrlem2 6378  axcnre 6439  peano2cn 6498  addcaniOLD 6506  negeui 6510  negid 6536  peano2re 6599  peano2rem 6605  renepnfOLD 6709  renemnfOLD 6711  nltmnf 6722  pnfge 6723  nltpnft 6741  ne0gt0 6801  lt0neg1 6857  le0neg1 6859  mulcani 6878  receui 6890  recgt0ii 6992  divgt0i2i 7041  ledivp1i 7089  ltdivp1i 7090  nnge1 7126  lt1nnn 7130  times2 7189  addltmul 7229  avgle 7231  lbinfm 7257  supxrbnd 7300  supxrgtmnf 7301  supxrre1 7302  supxrre2 7303  peano2nn0 7333  nn0lele2xi 7344  elnnz1 7364  peano2z 7375  peano2zm 7378  elnnnn0 7381  zltp1le 7390  zeo 7411  zneo 7412  dfuzi 7414  uzindOLD 7420  uzwo4OLD 7422  uzwo5OLD 7423  qsqueeze 7461  flge0nn0 7482  flge1nn 7483  btwnzge0 7486  flhalf 7487  ceim1l 7490  modfrac 7505  flmulnn0 7508  flmulnn0OLD 7509  icoshftf1oii 7578  icounlem 7581  peano2uzr 7617  uzwo 7624  uzwoOLD 7625  uzwo2 7626  infmssuzle 7634  infmssuzleOLD 7635  infmssuzcl 7636  fzprval 7687  fztpval 7688  om2uzsuci 7707  seq1rn 7735  ser1f 7741  limsupval 7772  seqzfval 7780  seq1seq02 7786  seqzp1 7791  seq0p1 7794  seqzval2 7796  seqzresval 7802  seqzres 7803  seqzres2 7804  exp0 7814  exp1 7816  expword2i 7850  expubnd 7853  sqval 7854  sqeq0 7858  resqcl 7866  sumsqne0i 7879  expnbnd 7901  nn0opthlem2 7915  sqrlem6 7928  sqrmsq2i 7956  imcj 8069  cjne0 8082  leabsi 8124  abs2dif 8154  facnn2 8191  faclbnd4lem3 8202  faclbnd5 8205  bcval4 8213  sumeq2 8245  sumeqfv 8257  dffsum 8258  fsum4 8285  csbfsumlem 8286  fsum0 8299  ser1ser0i 8308  serzrefi 8311  serz0 8313  serzmulci 8318  serzrelem 8321  binomlem2 8327  bcxmas 8336  climfnn 8352  climunii 8358  climshfti 8364  climshft2i 8366  climge0 8372  clim2serzi 8405  climserzlei 8407  climabslem 8408  climsupi 8415  iserzabslem 8438  cvgcmp2lem 8440  isumval2 8455  isumclim3 8461  infcvgaux2i 8481  arisumi 8487  expcnvlem2 8489  geolimilem 8497  geoisumr 8505  geoisum1c 8507  ivthlem7 8549  dsupivthlem 8553  efaddlem15 8614  efaddlem20 8619  efaddlem26 8625  efaddlem27 8626  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  absef01tllem 8649  eirrlem1 8651  eirrlem3 8653  eirrlem4 8654  eflegeolem2 8679  efcnlem1 8684  efcnlem2 8685  reeff1o 8691  resin4p 8701  recos4p 8702  sinbnd 8731  cosbnd 8732  sin01bndlem2 8734  cos01bndlem2 8736  sin02gt0 8744  sin4lt0 8747  znnenlem 8770  znnen 8771  ruclem15 8793  ruclem28 8806  ruclem30 8808  infxpidmlem1 8821  infxpidmlem11 8831  infxpidmlem12 8832  infdif 8837  infpss 8843  0opn 8870  topopn 8871  tgval 8886  unitg 8893  sn0top 8917  isopn2 8949  0cld 8954  iincld 8955  ntropn 8960  ntrval2 8962  cmclsopn 8969  cmntrcld 8970  clstop 8976  ntrtop 8977  cls0 8985  ntr0 8986  neiint 8995  neips 9003  cncnplem4 9054  cnconst 9057  metres 9100  blfval 9112  bl2in 9120  lmnn 9213  lmss 9231  caussi 9232  causs 9233  metcn4i 9250  fsumcnlem 9267  iscms2lem4 9270  lmcau 9274  bcthlem1 9277  bcthlem16 9292  gxsuc 9395  cnid 9435  mulid 9440  gapmlem 9461  vcoprne 9530  bafval 9555  nvnd 9651  ipfval 9691  ipval2lem3 9694  ipval2 9696  ipval2lem6 9700  4ipval3 9701  ipid 9702  ipcj 9706  ip0r 9709  ip1cnilem2 9713  ip1cnilem3 9714  ip1cnilem4 9715  islno 9753  lno0 9756  nmoge0 9769  nmlno0lem 9793  nmlnogt0 9797  blocni 9805  ipasslem2 9832  ipasslem8 9838  ipasslem9 9839  ipasslem11 9841  ajval 9863  ubthlem6 9877  minveclem24 9913  minveclem25 9914  minveclem26 9915  minveclem27 9916  minveclem28 9917  minveclem32 9921  minveceu 9928  pilem1 10020  pilem2 10021  sinhalfpilem 10028  sinperlem1 10035  sinper 10039  cosper 10040  sin2pim 10041  cos2pim 10042  sinmpi 10043  cosmpi 10044  sinppi 10045  cosppi 10046  efimpi 10047  sincosq1lem 10052  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  sinq12gt0t 10057  sinq34lt0t 10058  sincosq1eq 10059  abssinper 10062  sinkpi 10063  coskpi 10064  sineq0 10065  sineq0OLD 10066  cosh111lem1 10068  efifolem4 10079  efifolem5 10080  efifolem6 10081  efif1lem1 10084  efif1lem2 10085  shftefif1olem 10095  efper 10101  axgroth6 10137  twpar2 10149  oprabvaligg 10154  oprabco 10159  unfin 10166  finfin 10167  dif1en 10172  indexfi 10174  elsymgrn 10200  fbssint 10279  fsubbas 10281  fbunfip 10282  fbssfg 10285  extbas1 10291  filrn 10293  elfilmap 10312  ismnd2 10392  on1el3 10412  on1el4 10413  h2hcau 10481  h2hlm 10482  hvaddid2 10524  hvsubcan 10574  hvsubcan2 10575  hvsub0 10576  hi02 10596  hilid 10661  hcau 10684  hlim2 10693  chlimi 10737  hlimuniii 10741  hhsscms 10783  projlem10 10828  projlem12 10830  projlem13 10831  projlem15 10833  projlem25 10843  projlem26 10844  pjthlem7 10858  pjthlem8 10859  pjthlem11 10862  omlsilem 10877  pjpj0i 10888  pjoc1i 10897  shsupunss 10948  chsupunss 10949  shmodi 10996  chlejb1i 11032  h1dei 11106  h1de2bi 11110  h1de2ctlem 11111  h1de2ci 11112  spanunsni 11135  pjoml2i 11161  osumlem4 11216  pjorthi 11249  mayete3i 11308  mayete3OLDi 11309  hosubid1 11361  elcnop 11420  ellnop 11421  nmoprepnf 11431  elunop 11436  elhmop 11437  nmfnrepnf 11444  elcnfn 11446  ellnfn 11447  adjval 11451  nmopge0 11472  nmfnge0 11488  adj1 11494  adjeq 11496  lnop0 11527  nmlnop0iALT 11557  lnopmi 11562  nmophmi 11598  bdophmi 11599  lnopconi 11600  lnfnconi 11627  cnlnadjlem5 11641  cnlnadjeui 11647  unierri 11674  leoprf2 11698  leopnmid 11709  nmopleid 11710  opsqrlem6 11716  hmopidmchi 11723  stel 11786  hstel 11787  hstles 11803  hst0 11805  hstrlem6 11836  dmdbr2 11875  mdslj1i 11891  mdsl1i 11893  mdsl2i 11894  mdsl2bi 11895  cvmdi 11896  mdslmd1lem1 11897  mdslmd1lem2 11898  mdslmd1i 11901  mdslmd2i 11902  csmdsymi 11906  mdexchi 11907  superpos 11926  atomli 11954  atoml2i 11955  atordi 11956  irredlem1 11962  irredlem2 11963  irredlem3 11964  irredi 11966  atcvat4i 11969  atabsi 11973  mdsymlem1 11975  mdsymlem3 11977  mdsymlem5 11979  mdsymlem6 11980  sumdmdii 11987  sumdmdlem2 11991  dmdbr5ati 11994  dmdbr6ati 11995  mddmdin0i 12003  cdj3lem1 12006  cdj3lem2 12007  bnj1022 12884  bnj522 13261  bnj535 13265  bnj580 13301  bnj1253 13470  bnj1283 13476  nn0lt10b 13603  elfzp1b 13605  fseq1cl 13619  suprzcl 13658  nn0seqcvgd 13659  dvdsmul2 13677  dvdslelem 13692  divalglem0 13696  divalglem1 13697  divalglem2 13698  divalglem4 13699  divalglem5 13700  divalglem6 13701  divalglem8 13703  gcdcllem1 13718  algr0 13740  eucalgval 13749  mulgcdlem4 13759  1nprm 13769  epelcNEW 13826  predreseq 13890  predep 13903  wfr3g 13956  wfrlem5 13961  wfrlem14 13970  wfrlem15 13971  frr3g 13980  elno 13987  noxpsgn 13990  brtxp 14067  elfix 14077  condisd 14270  neiopne 14354  unfinsef 14375  fldsqcp2 14378  sqpeq 14383  tricptr 14385  prj1 14395  resrelfld 14448  cnveq3 14456  valpr 14499  repfuntw 14502  prl 14512  gepsup 14593  seinf 14594  domncnt 14624  prodeq2 14661  prodeqfv 14669  dffprod 14670  isppm 14715  symgfo 14730  trooo 14758  svli2 14826  topnem 14858  cexint2 14862  mapdiscnlem 14870  mapdiscn 14871  top2ind 14897  top2usne 14898  homindlem2 14899  subspemp 14903  efilcp 14922  efilcp2 14926  cnfilca 14927  rcfpfillem6 14933  limfillem1 14938  bwt2 14960  altretop 14997  cntrsetlem 14999  dmrngcmp 15098  taralt 15211  cptarc 15242  inttarcar 15278  elfiun 15369  finsschain 15373  omsubsuc2OLD 15387  omsublimOLD 15396  ntrcmp 15406  clscmp 15407  cldbnd 15410  subcls 15424  compsublem 15430  cptclsscpt 15432  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  connsub 15443  reconnlem1 15446  ivthALT 15454  2ndcctbss 15478  refref 15494  refssfne 15504  finptfin 15507  finlocfin 15509  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem4 15522  fbasfip 15556  isufil2 15565  ufileulem 15572  ufileu 15573  filufint 15574  ufilen 15579  filcon 15580  cnpfillim 15589  imaelfm 15591  fmfnfmlem4 15597  fclsfnflim 15614  fcluscomplem 15620  sfclusf 15624  tailfb 15639  unirep 15664  fnopabco 15711  f1elima 15719  upixp 15729  indexfiOLD 15755  inficl 15757  infmrgelb 15766  uzp1 15785  rddif 15798  absrdbnd 15799  sdclem2 15810  sdc 15811  fdc 15812  fsumlt1 15831  subspabs 15840  neificl 15841  blhalf 15846  mettrifi2 15848  geomcau 15849  metdcn 15853  iccshftri 15858  iccshftli 15860  iccdili 15862  icccntri 15864  oprpiece1res2 15881  cnss 15892  piececn 15894  tlmbr 15904  haustlmu 15906  txsubsp 15912  cnresoprab 15915  sstotbnd 15936  totbndss 15937  totbndbnd 15944  heiborlem1 15955  heiborlem13 15967  heiborlem16 15970  heiborlem30 15984  heiborlem36 15990  heiborlem40 15994  rrntotbnd 16022  phtpyid 16049  phtpycom 16050  phtpyco 16056  reparpht 16065  pco0 16077  pco1 16078  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorev 16087  pi1gp 16095  isrnghom 16119  prnc 16215  emhgrat 16297  snssl 16653  elstr 16714  elstrdiff 16720  stb2val2 16736  stb3val2 16740  stb3val3 16741  stb2xpl 16742  stb3xpl 16743  lubid 16807  glb0 16920  glbcon 17028  atompoint 17224  polsub 17320  pol0 17322  pol1 17323  2polval 17326  2polss 17327  3pol 17328  2pmaplub 17336  pnonsing 17343  polsubcl 17360

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 164  df-an 242

Copyright terms: Public domain