Theorem mpan2 700

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  mpanl2 711  mpanr12 715  mp3an3 911  mp3an23 914  a12lem1 1415  euor2 1477  eueq2 1964  eueq3 1965  sbccomg 2039  sbcralg 2044  sbcrexg 2045  unimax 2599  nnullss 2846  ord0eln0 3027  eldifpw 3133  ordeleqon 3144  ordsson 3145  ssnlim 3236  reldm0 3418  ssres2 3476  resdm 3483  iss 3487  resid 3490  ssrnres 3566  coi2 3615  relrelss 3618  funcnvres 3673  funimaex 3682  isarep1 3683  fnresin1 3707  fnresin2 3708  dffn2 3735  funssxp 3745  funbrfv 3861  ssimaex 3879  dmfco 3884  fvco 3885  fvopab3 3888  fvopab3ig 3889  fvopab4 3891  fvopab4sf 3893  fvopabn 3897  fvimacnvALT 3923  dff2 3930  dff3 3931  rnssopab 3939  fopabco 3946  fopabcos 3947  fsn 3948  fsn2 3950  fopabsn 3954  f1owe 4019  oprabvalig 4084  oprabval2gf 4086  1stval 4142  2ndval 4143  eqop 4164  2ndconst 4191  curry1 4193  curry2 4196  onopruni 4210  tfr3 4227  abianfplem 4262  abianfp 4263  oa0 4291  om0 4292  oa1suc 4300  om1 4312  oe1 4314  oe1m 4315  oarec 4332  omass 4347  oeoalem 4359  oeoelem 4361  nnarcl 4372  nneob 4395  ecelqsi 4432  mapval2 4476  mapsn 4486  mapss 4487  2dom 4568  xpdom1 4584  pw2en 4587  ac6sfilem2 4589  ac6sfi 4591  sbthlem2 4593  sbthlem7 4598  fodomr 4628  mapdom1 4639  mapdom2 4641  mapxpen 4642  xpmapenlem2 4644  xpmapenlem4 4646  xpmapenlem5 4647  mapunen 4649  phplem4 4658  php 4660  infn0 4679  unblem1 4686  unblem2 4687  unblem3 4688  unblem4 4689  isfinite2 4692  unfilem1 4694  unfilem2 4695  unfi 4697  unifi 4701  fiint 4703  fodomfi 4709  pwfilem 4713  pm54.43 4715  inf0 4751  infensuc 4784  trcl 4791  r1suc 4798  rankr1lem 4819  ssrankr1 4822  rankr1a 4823  rankxplim3 4860  scott0 4863  ac5b 4899  ac6lem 4900  fodom 4944  brdom3 4947  brdom5 4948  brdom4 4949  iundom 4958  cardval 4973  carden 4979  cardeq0 4980  card1 4981  unsnen 4983  carddomi 4984  unxpdomlem 4993  unxpdom2 4995  sucxpdom 4996  alephsuc 5016  alephnbtwn2 5019  alephsucdom 5030  alephle 5034  cardaleph 5035  iscard3 5038  alephfplem2 5047  alephfp 5050  cflem 5055  cflecard 5062  cfeq0 5064  cdaval 5069  cdadom1 5085  cdadom2 5086  cdafi 5088  cdainf 5089  nnacda 5090  mulidpi 5168  nlt1pi 5187  indpi 5188  1idpr 5287  prlem934a 5291  prlem934b 5292  prlem934 5293  0idsr 5360  1idsr 5361  00sr 5362  negexsr 5365  recexsrlem 5366  sqgt0sr 5369  map2psrpr 5374  supsrlem1 5379  supsrlem2 5380  axcnre 5440  peano2cn 5498  addcani 5505  negeui 5509  subaddi 5525  negid 5533  peano2re 5590  peano2rem 5596  renepnf 5691  renemnf 5692  ltpnf 5696  nltmnf 5701  pnfge 5702  nltpnft 5720  ne0gt0 5773  lt0neg1 5822  le0neg1 5824  mulcani 5842  receui 5853  divmuli 5857  recgt0ii 5954  divgt0i2i 6003  recp1lt1 6046  recreclt 6047  ledivp1i 6051  ltdivp1i 6052  nnge1 6088  nnle1eq1 6090  lt1nnn 6092  times2 6151  avgle 6190  lbinfm 6216  supxrbnd 6259  supxrgtmnf 6260  supxrre1 6261  supxrre2 6262  nn0le0eq0 6287  peano2nn0 6292  nn0ltp1le 6295  nn0ltlem1 6297  nn0lele2xi 6303  elnnz 6313  elznn0 6317  elnnz1 6323  znnnlt1 6324  peano2z 6334  peano2zm 6337  elnnnn0 6340  zltp1le 6349  zlem1lt 6351  zltlem1 6352  zeo 6370  zneo 6371  dfuzi 6373  uzindOLD 6379  uzwo4OLD 6381  uzwo5OLD 6382  rebtwnz 6394  qbtwnre 6418  qsqueeze 6420  flge0nn0 6441  flge1nn 6442  btwnzge0 6445  flhalf 6446  ceim1l 6449  fldiv 6456  modfrac 6464  flmulnn0 6467  flmulnn0OLD 6468  monoord 6482  icoshftf1oii 6536  icounlem 6539  eluzaddi 6563  eluzsubi 6564  peano2uzr 6575  uzwo 6582  uzwoOLD 6583  uzwo2 6584  infmssuzle 6592  infmssuzleOLD 6593  infmssuzcl 6594  fz01en 6623  om2uzsuci 6659  seq1m1 6684  seq1rn 6687  ser1f 6693  limsupval 6724  seqzfval 6732  seq1seq02 6738  seqz1 6742  seqzp1 6743  seqzm1 6744  seq0p1 6746  seqzval2 6748  seqzresval 6754  seqzres 6755  seqzres2 6756  exp0 6766  exp1 6768  expm1t 6778  expword2i 6802  expubnd 6805  sqval 6806  sqeq0 6810  resqcl 6818  sumsqne0i 6831  expnbnd 6852  nn0opthlem2 6866  sqrlem5 6878  sqrlem6 6879  sqrlem13 6886  sqrmsq2i 6907  imcj 7020  cjne0 7033  sqabs 7071  leabsi 7075  abs2dif 7105  facnn2 7142  facndiv 7146  faclbnd2 7149  faclbnd4lem1 7151  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd5 7156  bcval4 7164  bcnp11 7168  bcnp1n 7169  sumeq2 7188  sumeqfv 7200  dffsum 7201  serzfsum 7207  fsump1i 7209  fsum4 7228  csbfsumlem 7229  fsum0 7242  ser1ser0i 7251  serzrefi 7254  serz0 7256  serzsplit 7259  serzmulci 7261  serzrelem 7264  binomlem2 7270  bcxmas 7279  climfnn 7295  climunii 7301  climshfti 7307  climshft2i 7309  iserzshft2i 7310  climge0 7315  clim2serzi 7348  climserzlei 7350  climabslem 7351  climubii 7356  climsupi 7358  climcaui 7359  caucvgi 7366  serzf0i 7372  iserzabslem 7381  cvgcmp2lem 7383  isumval2 7398  isumclim3 7404  infcvgaux2i 7424  infcvglem1 7425  arisumi 7430  expcnvlem2 7432  geoseri 7439  geolimilem 7440  geoisumr 7448  geoisum1c 7450  cvgratlem1ALT 7452  fsum0diaglem1 7461  fsum0diag2 7464  fsum0diag4 7466  ivthlem6 7491  ivthlem7 7492  dsupivthlem 7496  efseq0ex 7516  efaddlem1 7543  efaddlem15 7557  efaddlem16 7558  efaddlem20 7562  efaddlem26 7568  efaddlem27 7569  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  absef01tllem 7592  eirrlem1 7594  eirrlem3 7596  eirrlem4 7597  efgt0i 7612  eflegeolem2 7622  efcnlem1 7627  efcnlem2 7628  reeff1o 7634  efi4p 7643  resin4p 7644  recos4p 7645  sinbnd 7674  cosbnd 7675  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  sin4lt0 7690  absefib 7693  efieq1re 7694  xpnnen 7711  znnenlem 7713  znnen 7714  unben 7717  ruclem15 7736  ruclem28 7749  ruclem30 7751  infxpidmlem1 7764  infxpidmlem11 7774  infxpidmlem12 7775  infdif 7780  infpss 7786  infmap2 7793  0opn 7813  topopn 7814  tgval 7828  unitg 7835  sn0top 7859  cctop 7862  isopn2 7883  0cld 7888  iincld 7889  ntropn 7894  ntrval2 7896  cmclsopn 7903  cmntrcld 7904  clstop 7910  ntrtop 7911  cls0 7919  ntr0 7920  neiint 7929  neips 7937  cncnplem4 7987  cnconst 7990  metres 8033  metxp 8044  blfval 8045  bl2in 8053  lmbrf 8141  lmnn 8146  iscauf 8150  iscau5 8152  iscaunns 8155  lmsslem 8163  lmss 8164  caussi 8165  causs 8166  lmclimnn 8175  metcn4i 8183  oprcn 8188  fsumcnlem 8200  iscms2lem4 8203  lmcau 8207  bcthlem1 8210  bcthlem16 8225  gxoprval 8313  gxnval 8316  gx1 8318  gxsuc 8328  cnid 8368  mulid 8373  vcoprne 8445  bafval 8470  invfval 8508  nvnd 8566  ipfval 8606  ipval2lem3 8609  ipval2 8611  ipval2lem6 8615  4ipval3 8616  ipid 8617  ipcj 8621  ip0r 8624  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem4 8630  islno 8668  lno0 8671  nmoge0 8684  nmlno0lem 8708  nmlnogt0 8712  blocni 8720  ipasslem2 8747  ipasslem8 8753  ipasslem9 8754  ipasslem11 8756  ajval 8778  ubthlem6 8792  minveclem24 8828  minveclem25 8829  minveclem26 8830  minveclem27 8831  minveclem28 8832  minveclem32 8836  minveceu 8843  pilem1 8938  pilem2 8939  sinhalfpilem 8946  sinperlem1 8953  sinper 8957  cosper 8958  sin2pim 8959  cos2pim 8960  sinmpi 8961  cosmpi 8962  sinppi 8963  cosppi 8964  efimpi 8965  sincosq1lem 8970  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  sinq12gt0t 8975  sinq34lt0t 8976  sincosq1eq 8977  abssinper 8980  sinkpi 8981  coskpi 8982  sineq0 8983  sineq0OLD 8984  cosh111lem1 8986  efifolem4 8997  efifolem5 8998  efifolem6 8999  efif1lem1 9002  efif1lem2 9003  shftefif1olem 9013  efper 9019  h2hcau 9124  h2hlm 9125  hvaddid2 9167  hvsubcan 9217  hvsubcan2 9218  hvsub0 9219  hi02 9239  hilid 9304  hcau 9327  hlim2 9336  chlimi 9380  hlimuniii 9384  hhsscms 9426  projlem10 9471  projlem12 9473  projlem13 9474  projlem15 9476  projlem25 9486  projlem26 9487  pjthlem7 9501  pjthlem8 9502  pjthlem11 9505  omlsilem 9520  pjpj0i 9531  pjoc1i 9540  shsupunss 9591  chsupunss 9592  shmodi 9639  chlejb1i 9675  h1dei 9749  h1de2bi 9753  h1de2ctlem 9754  h1de2ci 9755  spanunsni 9778  pjoml2i 9804  osumlem4 9859  pjorthi 9892  mayete3i 9951  mayete3OLDi 9952  hosubid1 10004  elcnop 10063  ellnop 10064  nmoprepnf 10074  elunop 10079  elhmop 10080  nmfnrepnf 10087  elcnfn 10089  ellnfn 10090  adjval 10094  nmopge0 10115  nmfnge0 10131  adj1 10137  adjeq 10139  lnop0 10169  nmlnop0iALT 10199  lnopmi 10204  nmophmi 10240  bdophmi 10241  lnopconi 10242  lnfnconi 10269  cnlnadjlem5 10283  cnlnadjeui 10289  unierri 10316  leoprf2 10340  leopnmid 10351  nmopleid 10352  hmopidmchi 10359  stel 10422  hstel 10423  hstles 10439  hst0 10441  hstrlem6 10472  dmdbr2 10511  mdslj1i 10527  mdsl1i 10529  mdsl2i 10530  mdsl2bi 10531  cvmdi 10532  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd1i 10537  mdslmd2i 10538  csmdsymi 10542  mdexchi 10543  superpos 10562  atomli 10591  atoml2i 10592  atordi 10593  irredlem1 10599  irredlem2 10600  irredlem3 10601  irredi 10603  atcvat4i 10606  atabsi 10610  mdsymlem1 10612  mdsymlem3 10614  mdsymlem5 10616  mdsymlem6 10617  sumdmdii 10624  sumdmdlem2 10628  dmdbr5ati 10631  dmdbr6ati 10632  mddmdin0i 10640  cdj3lem1 10643  cdj3lem2 10644  elsymgrn 10686  oprabvaligg 10729  neiopne 10757  twpar2 10773  unfinsef 10775  fldsqcp2 10780  sqpeq 10786  tricptr 10788  unfin 10797  finfin 10798  prj1 10809  domncnt 10872  isppm 10917  ismnd2 10928  on1el3 10962  on1el4 10963  topnem 11008  mapdiscn 11014  top2ind 11050  top2usne 11051  homindlem2 11052  subspemp 11060  efilcp 11083  efilcp2 11087  cnfilca 11088  rcfpfillem6 11094  limfillem1 11101  bwt2 11123  altretop 11144  dmrngcmp 11205  elfiun 11421  finsschain 11425  omsubsuc2 11439  omsublim 11448  ntrcmp 11458  clscmp 11459  cldbnd 11462  subcls 11481  compsublem 11487  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  alexsublem3 11498  alexsublem4 11499  connsub 11502  reconnlem1 11507  ivthALT 11515  2ndcctbss 11539  refref 11555  refssfne 11565  finptfin 11568  finlocfin 11570  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem4 11583  fbssint 11626  fbasfip 11627  fsubbas 11630  fbunfip 11631  fbssfg 11635  extbas1 11641  filrn 11643  isufil2 11650  ufileulem 11657  ufileu 11658  filufint 11659  ufilen 11664  filcon 11665  cnpfillim 11686  elfilmap 11690  imaelfm 11695  fmfnfmlem4 11703  fclsfnflim 11726  fcluscomplem 11732  sfclusf 11736  tailfb 11762  gapmlem 11783  fnopabco 11810  oprabco 11811  f1elima 11818  upixp 11823  indexf 11847  inficl 11849  uzp1 11863  rddif 11869  absrdbnd 11870  sdclem2 11876  sdc 11877  fsumlt1 11894  subspabs 11903  neificl 11904  blhalf 11911  mettrifi2 11913  geomcau 11914  metdcn 11918  iccshftri 11923  iccshftli 11925  iccdili 11927  icccntri 11929  cnss 11953  piececn 11955  tlmbr 11965  haustlmu 11967  txsubsp 11983  sstotbnd 11992  totbndss 11993  totbndbnd 12000  heiborlem1 12011  heiborlem13 12023  heiborlem16 12026  heiborlem30 12040  heiborlem36 12046  heiborlem40 12050  rrntotbnd 12078  phtpyid 12091  phtpycom 12092  phtpyco 12098  emhgrat 12201

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