Theorem mpan2 694

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanl2 705  mp3an3 902  mp3an23 905  a12lem1 1369  euor2 1430  eueq2 1909  eueq3 1910  sbccomg 1979  sbcralg 1984  sbcrexg 1985  unimax 2522  nnullss 2758  eldifpw 2900  ordeleqon 2980  ordsson 2981  ord0eln0 3013  ssnlim 3157  reldm0 3320  ssres2 3370  resdm 3377  iss 3381  resid 3384  ssrnres 3467  coi2 3497  funcnvres 3554  funimaex 3562  isarep1 3563  fnresin1 3587  fnresin2 3588  fnf 3614  funssxp 3623  funbrfv 3735  ssimaex 3753  dmfco 3758  fvco 3759  fvopab3 3762  fvopab3ig 3763  fvopab4 3765  fvopab4sf 3767  fvopabn 3771  fvimacnvALT 3794  dff4 3801  dff2 3802  rnssopab 3810  fopabco 3817  fopabcos 3818  fsn 3819  fsn2 3821  fopabsn 3825  f1owe 3890  tfr3 3911  abianfplem 3946  abianfp 3947  oprabvalig 4009  oprabval2gf 4011  1stval 4065  2ndval 4066  2ndconst 4081  curry1 4082  eqop 4088  oa0 4139  om0 4140  oa1suc 4148  om1 4160  oe1 4162  oe1m 4163  oarec 4180  omass 4195  nnarcl 4216  nneob 4239  ecelqsi 4276  mapval2 4319  mapsn 4329  mapss 4330  2dom 4408  xpdom1 4423  pw2en 4426  sbthlem2 4428  sbthlem7 4433  fodomr 4463  2pwuninel 4465  mapdom1 4472  mapdom2 4474  mapxpen 4475  xpmapenlem2 4477  xpmapenlem4 4479  xpmapenlem5 4480  mapunen 4482  limensuci 4486  phplem4 4491  php 4493  infn0 4512  unblem1 4517  unblem2 4518  unblem3 4519  unblem4 4520  isfinite2 4523  unfilem1 4524  unfilem2 4525  unfi 4528  unifi 4532  fiint 4534  fodomfi 4540  pwfilem 4544  pm54.43 4546  inf0 4578  infensuc 4610  trcl 4617  r1suc 4624  rankr1lem 4645  ssrankr1 4648  rankr1a 4649  rankxplim3 4686  scott0 4689  ac5b 4725  ac6lem 4726  fodom 4770  brdom3 4773  brdom5 4774  brdom4 4775  iundom 4784  cardval 4798  carden 4803  cardeq0 4804  card1 4805  carddomi 4807  unxpdomlem 4815  unxpdom2 4817  sucxpdom 4818  alephsuc 4838  alephnbtwn2 4841  alephsucdom 4852  alephle 4856  cardaleph 4857  iscard3 4860  alephfplem2 4869  alephfp 4872  cflem 4877  cflecard 4884  cfeq0 4886  cdavalt 4891  cdaen 4896  cdadom1 4905  cdadom2 4906  cdafi 4908  cdainf 4909  mulidpi 4986  nlt1pi 5005  indpi 5006  mulidpq 5041  1idpr 5105  prlem934a 5109  prlem934b 5110  prlem934 5111  0idsr 5178  1idsr 5179  00sr 5180  negexsr 5183  recexsrlem 5184  sqgt0sr 5187  map2psrpr 5192  supsrlem1 5197  supsrlem2 5198  addresr 5228  mulresr 5229  ax0id 5253  ax1id 5254  axcnre 5258  peano2cn 5316  addcan 5323  negeu 5327  subadd 5343  negidt 5351  peano2re 5408  peano2rem 5414  renepnft 5510  renemnft 5511  ltpnft 5515  nltmnft 5520  pnfget 5521  nltpnftt 5539  ne0gt0t 5593  lt0neg1t 5641  le0neg1t 5643  mulcan 5659  receu 5670  divmul 5674  recgt0i 5770  divgt0i2 5813  reclt1t 5846  recp1lt1 5849  recrecltt 5850  ledivp1 5854  ltdivp1 5855  nnge1t 5891  nnle1eq1t 5893  lt1nnn 5895  nnleltp1t 5901  times2t 5952  halfpm6th 5979  2halvest 5986  halfaddsubt 5988  nominpos 5990  avglet 5991  lbinfm 5995  supxrbnd 6038  supxrgtmnf 6039  supxrre1 6040  supxrre2 6041  nn0le0eq0t 6066  peano2nn0 6071  nn0ltp1let 6074  nn0ltlem1t 6076  nn0lele2x 6082  elnnz 6092  elznn0 6096  elnnz1 6102  znnnlt1t 6103  peano2z 6113  peano2zm 6116  elnnnn0 6119  zltp1let 6128  zlem1ltt 6130  zltlem1t 6131  nneo 6144  zeot 6146  zneo 6147  zneoOLD 6148  dfuz 6150  uzindOLD 6156  uzwo4OLD 6158  uzwo5OLD 6159  rebtwnz 6170  flge0nn0t 6185  flge1nnt 6186  btwnzge0t 6188  flhalft 6189  ceim1lt 6192  qbtwnre 6216  qsqueeze 6218  monoord 6231  om2uzsuc 6233  seq1m1 6256  seq1rn 6259  ser1ft 6265  icoshftf1oi 6342  icounlem 6345  eluzaddi 6368  eluzsubi 6369  peano2uzr 6380  uzwo 6387  uzwoOLD 6388  uzwo2 6389  infmssuzle 6397  infmssuzcl 6398  limsupvalt 6461  seqzfval 6469  seq1seq02t 6475  seqz1 6479  seqzp1 6480  seqzm1 6481  seq0p1 6483  seqzval2t 6485  seqzresval 6491  seqzres 6492  seqzres2 6493  exp0t 6503  exp1t 6505  expm1t 6515  expword2it 6536  expubndt 6539  sqvalt 6540  resqclt 6552  sumsqne0 6565  expnbndt 6585  nn0opthlem2 6595  sqrlem5 6607  sqrlem6 6608  sqrlem13 6615  sqrmsq2 6636  crutOLD 6669  crretOLD 6703  crimtOLD 6705  imret 6710  recjt 6753  imcjt 6754  cjne0t 6766  leabs 6807  abs2dift 6839  facnn2t 6876  facndivt 6880  faclbnd2 6883  faclbnd4lem1 6885  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd5 6890  bcval4t 6899  bcnp11t 6903  bcnp1nt 6904  sumeq2 6923  sumeqfv 6935  dffsum 6936  serzfsum 6942  fsump1 6944  fsum4 6963  csbfsumlem 6964  fsum0 6977  ser1ser0 6986  serzref 6989  serz0 6991  serzsplit 6994  serzmulc 6996  serzrelem 6999  binomlem2 7005  bcxmas 7014  climfnn 7030  climunii 7035  climshft 7041  climshft2 7043  iserzshft2 7044  climge0 7049  climaddlem3 7052  clim2serz 7081  climserzle 7083  climabslem 7084  climubi 7089  climsup 7091  climcau 7092  caucvg 7099  caucvg3lem 7102  serzf0 7105  ser1f0 7106  iserzabslem 7114  cvgcmp2lem 7116  isumval2t 7130  isumclim3t 7135  infcvgaux2 7155  infcvglem1 7156  fnsmnt 7161  expcnvlem2 7163  geoser 7169  geolimilem 7170  geoisumr 7178  geoisum1c 7180  cvgratlem1ALT 7182  fsum0diaglem1 7191  fsum0diag2 7194  fsum0diag4 7196  ivthlem6 7221  ivthlem7 7222  dsupivthlem 7226  ivthlem6OLD 7230  ivthlem7OLD 7231  efseq0ex 7253  erelem3 7263  efaddlem1 7280  efaddlem15 7294  efaddlem16 7295  efaddlem20 7299  efaddlem26 7305  efaddlem27 7306  ef01tllem1 7325  ef01tllem2 7326  absef01tllem 7328  eirrlem1 7330  eirrlem3 7332  eirrlem4 7333  efgt0 7345  eflegeolem2 7354  efcnlem1 7359  efcnlem2 7360  reeff1o 7368  efi4pt 7377  resin4pt 7378  recos4pt 7379  efivalt 7389  sinbndt 7407  cosbndt 7408  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  cos2bnd 7417  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  sin4lt0 7423  xpnnen 7441  znnenlem 7443  znnenlemOLD 7444  znnen 7445  unben 7448  ruclem15 7467  ruclem28 7480  ruclem30 7482  infxpidmlem1 7495  infxpidmlem11 7505  infxpidmlem12 7506  infdif 7511  infmap2 7523  0opnt 7543  topopn 7544  tgvalt 7558  unitgt 7565  sn0top 7589  fctop 7592  cctop 7594  isopn2 7615  0cld 7620  iincld 7621  ntropn 7626  ntrval2 7628  cmclsopn 7635  cmntrcld 7636  clstop 7642  ntrtop 7643  cls0 7651  neiint 7660  neips 7668  cncnplem4 7716  cnconst 7719  metres 7763  metxp 7774  blfval 7775  bl2in 7783  blex 7789  opnm 7800  ioo2bl 7851  lmbrf 7868  lmnn 7873  iscauf 7877  iscau5 7878  lmsslem 7887  lmss 7888  caussi 7889  causs 7890  lmclimnn 7899  metcn4i 7906  oprcn 7911  fsumcnlem 7923  iscms2lem4 7926  lmcau 7930  bcthlem1 7933  bcthlem16 7948  bcthlem21 7953  cnid 8064  mulid 8069  vcoprne 8136  bafval 8161  invfval 8201  nvnd 8257  ipfval 8286  ipval2lem3 8289  ipval2 8291  ipval2lem6 8295  4ipval3 8296  ipid 8297  ipcj 8301  ip0r 8304  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem4 8310  islno 8348  lno0 8351  nmoge0 8362  nmlno0lem 8385  nmlnogt0 8389  blocni 8396  ipasslem2 8422  ipasslem8 8428  ipasslem9 8429  ipasslem11 8431  ubthlem6 8465  minveclem24 8499  minveclem25 8500  minveclem26 8501  minveclem27 8502  minveclem28 8503  minveclem32 8507  minveclem38 8513  minveceu 8514  pilem1 8590  pilem2 8591  sinhalfpilem 8598  sinperlem1 8605  sinper 8609  cosper 8610  sin2pim 8611  cos2pim 8612  sinmpi 8613  cosmpi 8614  efimpi 8615  sincosq1lem 8620  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  sincosq1eq 8626  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  efifolem4 8640  efifolem5 8641  efifolem6 8642  efifolem7 8643  efif1lem1 8645  efif1lem2 8646  shftefif1olem 8661  shftefif1olemOLD 8662  efper 8669  h2hcau 8788  h2hlm 8789  hvaddid2t 8813  hvsubcant 8862  hvsubcan2t 8863  hvsub0t 8864  hi02t 8884  hilid 8949  hcau 8972  hlim2 8981  chlim 9025  hlimunii 9029  hhsscms 9067  projlem10 9111  projlem12 9113  projlem13 9114  projlem15 9116  projlem25 9126  projlem26 9127  pjthlem7 9140  pjthlem8 9141  pjthlem11 9144  omlsilem 9159  pjpj0 9170  pjoc1 9179  shsupunss 9230  chsupunss 9231  shmod 9278  chlejb1 9314  h1det 9388  h1de2b 9392  h1de2bOLD 9393  h1de2ctlem 9394  h1de2ct 9395  spanunsn 9419  pjoml2 9445  osumlem4 9498  pjorth 9531  mayete3 9590  hosubid1t 9641  elcnopt 9700  ellnopt 9701  nmoprepnf 9711  elunopt 9716  elhmopt 9717  nmfnrepnf 9724  elcnfnt 9726  ellnfnt 9727  adjvalt 9731  nmopge0t 9751  nmfnge0t 9767  adjt 9773  adjeqt 9775  lnop0t 9806  nmlnop0ALT 9835  lnopm 9840  nmophm 9876  bdophm 9877  lnopcon 9878  lnfncon 9905  cnlnadjlem5 9919  cnlnadjeu 9925  nmoptri 9941  nmopcoadj 9948  unierr 9950  leoprf2t 9972  leopnmidt 9982  nmopleidt 9983  hmopidmch 9990  stelt 10051  hstelt 10052  hstle1t 10063  hstlest 10068  hst0t 10070  strlem3a 10089  strlem5 10092  strlem6 10093  hstrlem6 10101  jplem1 10105  dmdbr2 10140  mdslj1 10154  mdsl1 10156  mdsl2 10157  mdsl2b 10158  cvmd 10159  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd1 10164  mdslmd2 10165  csmdsym 10169  mdexch 10170  superpos 10189  atoml 10217  atoml2 10218  atord 10219  irredlem1 10225  irredlem2 10226  irredlem3 10227  irred 10229  atcvat4 10232  atabs 10236  mdsymlem1 10238  mdsymlem3 10240  mdsymlem5 10242  mdsymlem6 10243  sumdmdi 10249  sumdmdlem2 10253  dmdbr5at 10255  dmdbr6at 10256  mddmdin0 10263  cdj3lem1 10266  cdj3lem2 10267  elsymgrn 10306  oprabvaligg 10341  neiopne 10369  topnem 10394  mapdiscn 10398  efilcp 10445  efilcp2 10450  cnfilca 10451  emhgrat 10611

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