Theorem mpan2 695

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 706  mp3an3 903  mp3an23 906  a12lem1 1374  euor2 1435  eueq2 1914  eueq3 1915  sbccomg 1985  sbcralg 1990  sbcrexg 1991  unimax 2527  nnullss 2763  eldifpw 2905  ordeleqon 2985  ordsson 2986  ord0eln0 3018  ssnlim 3162  reldm0 3326  ssres2 3378  resdm 3385  iss 3389  resid 3392  ssrnres 3473  coi2 3503  funcnvres 3560  funimaex 3568  isarep1 3569  fnresin1 3593  fnresin2 3594  fnf 3620  funssxp 3629  funbrfv 3741  ssimaex 3759  dmfco 3764  fvco 3765  fvopab3 3768  fvopab3ig 3769  fvopab4 3771  fvopab4sf 3773  fvopabn 3777  fvimacnvALT 3800  dff4 3807  dff2 3808  rnssopab 3816  fopabco 3823  fopabcos 3824  fsn 3825  fsn2 3827  fopabsn 3831  f1owe 3896  tfr3 3917  abianfplem 3952  abianfp 3953  oprabvalig 4015  oprabval2gf 4017  1stval 4071  2ndval 4072  2ndconst 4087  curry1 4088  eqop 4094  oa0 4145  om0 4146  oa1suc 4154  om1 4166  oe1 4168  oe1m 4169  oarec 4186  omass 4201  nnarcl 4222  nneob 4245  ecelqsi 4282  mapval2 4325  mapsn 4335  mapss 4336  2dom 4414  xpdom1 4429  pw2en 4432  sbthlem2 4434  sbthlem7 4439  fodomr 4469  mapdom1 4478  mapdom2 4480  mapxpen 4481  xpmapenlem2 4483  xpmapenlem4 4485  xpmapenlem5 4486  mapunen 4488  limensuci 4492  phplem4 4497  php 4499  infn0 4518  unblem1 4523  unblem2 4524  unblem3 4525  unblem4 4526  isfinite2 4529  unfilem1 4530  unfilem2 4531  unfi 4534  unifi 4538  fiint 4540  fodomfi 4546  pwfilem 4550  pm54.43 4552  inf0 4586  infensuc 4618  trcl 4625  r1suc 4632  rankr1lem 4653  ssrankr1 4656  rankr1a 4657  rankxplim3 4694  scott0 4697  ac5b 4733  ac6lem 4734  fodom 4778  brdom3 4781  brdom5 4782  brdom4 4783  iundom 4792  cardval 4806  carden 4811  cardeq0 4812  card1 4813  carddomi 4815  unxpdomlem 4823  unxpdom2 4825  sucxpdom 4826  alephsuc 4846  alephnbtwn2 4849  alephsucdom 4860  alephle 4864  cardaleph 4865  iscard3 4868  alephfplem2 4877  alephfp 4880  cflem 4885  cflecard 4892  cfeq0 4894  cdavalt 4899  cdaen 4904  cdadom1 4913  cdadom2 4914  cdafi 4916  cdainf 4917  mulidpi 4994  nlt1pi 5013  indpi 5014  mulidpq 5049  1idpr 5113  prlem934a 5117  prlem934b 5118  prlem934 5119  0idsr 5186  1idsr 5187  00sr 5188  negexsr 5191  recexsrlem 5192  sqgt0sr 5195  map2psrpr 5200  supsrlem1 5205  supsrlem2 5206  addresr 5236  mulresr 5237  ax0id 5261  ax1id 5262  axcnre 5266  peano2cn 5324  addcan 5331  negeu 5335  subadd 5351  negidt 5359  peano2re 5416  peano2rem 5422  renepnft 5518  renemnft 5519  ltpnft 5523  nltmnft 5528  pnfget 5529  nltpnftt 5547  ne0gt0t 5601  lt0neg1t 5649  le0neg1t 5651  mulcan 5667  receu 5678  divmul 5682  recgt0i 5778  divgt0i2 5821  reclt1t 5854  recp1lt1 5857  recrecltt 5858  ledivp1 5862  ltdivp1 5863  nnge1t 5899  nnle1eq1t 5901  lt1nnn 5903  nnleltp1t 5909  times2t 5960  halfpm6th 5987  2halvest 5994  halfaddsubt 5996  nominpos 5998  avglet 5999  lbinfm 6003  supxrbnd 6046  supxrgtmnf 6047  supxrre1 6048  supxrre2 6049  nn0le0eq0t 6074  peano2nn0 6079  nn0ltp1let 6082  nn0ltlem1t 6084  nn0lele2x 6090  elnnz 6100  elznn0 6104  elnnz1 6110  znnnlt1t 6111  peano2z 6121  peano2zm 6124  elnnnn0 6127  zltp1let 6136  zlem1ltt 6138  zltlem1t 6139  nneo 6152  zeot 6154  zneo 6155  zneoOLD 6156  dfuz 6158  uzindOLD 6164  uzwo4OLD 6166  uzwo5OLD 6167  rebtwnz 6178  flge0nn0t 6193  flge1nnt 6194  btwnzge0t 6196  flhalft 6197  ceim1lt 6200  qbtwnre 6224  qsqueeze 6226  monoord 6239  om2uzsuc 6241  seq1m1 6264  seq1rn 6267  ser1ft 6273  icoshftf1oi 6350  icounlem 6353  eluzaddi 6376  eluzsubi 6377  peano2uzr 6388  uzwo 6395  uzwoOLD 6396  uzwo2 6397  infmssuzle 6405  infmssuzcl 6406  limsupvalt 6469  seqzfval 6477  seq1seq02t 6483  seqz1 6487  seqzp1 6488  seqzm1 6489  seq0p1 6491  seqzval2t 6493  seqzresval 6499  seqzres 6500  seqzres2 6501  exp0t 6511  exp1t 6513  expm1t 6523  expword2it 6544  expubndt 6547  sqvalt 6548  resqclt 6560  sumsqne0 6573  expnbndt 6593  nn0opthlem2 6603  sqrlem5 6615  sqrlem6 6616  sqrlem13 6623  sqrmsq2 6644  crutOLD 6677  crretOLD 6711  crimtOLD 6713  imret 6718  recjt 6761  imcjt 6762  cjne0t 6774  leabs 6815  abs2dift 6847  facnn2t 6884  facndivt 6888  faclbnd2 6891  faclbnd4lem1 6893  faclbnd4lem3 6895  faclbnd4lem4 6896  faclbnd5 6898  bcval4t 6907  bcnp11t 6911  bcnp1nt 6912  sumeq2 6931  sumeqfv 6943  dffsum 6944  serzfsum 6950  fsump1 6952  fsum4 6971  csbfsumlem 6972  fsum0 6985  ser1ser0 6994  serzref 6997  serz0 6999  serzsplit 7002  serzmulc 7004  serzrelem 7007  binomlem2 7013  bcxmas 7022  climfnn 7038  climunii 7043  climshft 7049  climshft2 7051  iserzshft2 7052  climge0 7057  climaddlem3 7060  clim2serz 7089  climserzle 7091  climabslem 7092  climubi 7097  climsup 7099  climcau 7100  caucvg 7107  caucvg3lem 7110  serzf0 7113  ser1f0 7114  iserzabslem 7122  cvgcmp2lem 7124  isumval2t 7138  isumclim3t 7143  infcvgaux2 7163  infcvglem1 7164  fnsmnt 7169  expcnvlem2 7171  geoser 7177  geolimilem 7178  geoisumr 7186  geoisum1c 7188  cvgratlem1ALT 7190  fsum0diaglem1 7199  fsum0diag2 7202  fsum0diag4 7204  ivthlem6 7229  ivthlem7 7230  dsupivthlem 7234  ivthlem6OLD 7238  ivthlem7OLD 7239  efseq0ex 7261  erelem3 7271  efaddlem1 7288  efaddlem15 7302  efaddlem16 7303  efaddlem20 7307  efaddlem26 7313  efaddlem27 7314  ef01tllem1 7333  ef01tllem2 7334  absef01tllem 7336  eirrlem1 7338  eirrlem3 7340  eirrlem4 7341  efgt0 7353  eflegeolem2 7362  efcnlem1 7367  efcnlem2 7368  reeff1o 7376  efi4pt 7385  resin4pt 7386  recos4pt 7387  efivalt 7397  sinbndt 7415  cosbndt 7416  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos2bnd 7425  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  sin4lt0 7431  xpnnen 7449  znnenlem 7451  znnenlemOLD 7452  znnen 7453  unben 7456  ruclem15 7475  ruclem28 7488  ruclem30 7490  infxpidmlem1 7503  infxpidmlem11 7513  infxpidmlem12 7514  infdif 7519  infmap2 7531  0opnt 7551  topopn 7552  tgvalt 7566  unitgt 7573  sn0top 7597  fctop 7600  cctop 7602  isopn2 7623  0cld 7628  iincld 7629  ntropn 7634  ntrval2 7636  cmclsopn 7643  cmntrcld 7644  clstop 7650  ntrtop 7651  cls0 7659  ntr0 7660  neiint 7669  neips 7677  cncnplem4 7727  cnconst 7730  metres 7775  metxp 7786  blfval 7787  bl2in 7795  blex 7801  opnm 7812  ioo2bl 7864  lmbrf 7882  lmnn 7887  iscauf 7891  iscau5 7893  lmsslem 7903  lmss 7904  caussi 7905  causs 7906  lmclimnn 7915  metcn4i 7922  oprcn 7927  fsumcnlem 7939  iscms2lem4 7942  lmcau 7946  bcthlem1 7949  bcthlem16 7964  bcthlem21 7969  cnid 8079  mulid 8084  vcoprne 8150  bafval 8175  invfval 8213  nvnd 8270  ipfval 8299  ipval2lem3 8302  ipval2 8304  ipval2lem6 8308  4ipval3 8309  ipid 8310  ipcj 8314  ip0r 8317  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem4 8323  islno 8361  lno0 8364  nmoge0 8375  nmlno0lem 8398  nmlnogt0 8402  blocni 8409  ipasslem2 8435  ipasslem8 8441  ipasslem9 8442  ipasslem11 8444  ubthlem6 8478  minveclem24 8512  minveclem25 8513  minveclem26 8514  minveclem27 8515  minveclem28 8516  minveclem32 8520  minveclem38 8526  minveceu 8527  pilem1 8609  pilem2 8610  sinhalfpilem 8617  sinperlem1 8624  sinper 8628  cosper 8629  sin2pim 8630  cos2pim 8631  sinmpi 8632  cosmpi 8633  efimpi 8634  sincosq1lem 8639  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincosq1eq 8645  sincos4thpi 8646  sincos6thpi 8647  cosh111lem1 8648  efifolem4 8659  efifolem5 8660  efifolem6 8661  efifolem7 8662  efif1lem1 8664  efif1lem2 8665  shftefif1olem 8680  efper 8686  h2hcau 8788  h2hlm 8789  hvaddid2t 8831  hvsubcant 8880  hvsubcan2t 8881  hvsub0t 8882  hi02t 8902  hilid 8967  hcau 8990  hlim2 8999  chlim 9043  hlimunii 9047  hhsscms 9089  projlem10 9134  projlem12 9136  projlem13 9137  projlem15 9139  projlem25 9149  projlem26 9150  pjthlem7 9163  pjthlem8 9164  pjthlem11 9167  omlsilem 9182  pjpj0 9193  pjoc1 9202  shsupunss 9253  chsupunss 9254  shmod 9301  chlejb1 9337  h1det 9411  h1de2b 9415  h1de2bOLD 9416  h1de2ctlem 9417  h1de2ct 9418  spanunsn 9442  pjoml2 9468  osumlem4 9521  pjorth 9554  mayete3 9613  hosubid1t 9664  elcnopt 9723  ellnopt 9724  nmoprepnf 9734  elunopt 9739  elhmopt 9740  nmfnrepnf 9747  elcnfnt 9749  ellnfnt 9750  adjvalt 9754  nmopge0t 9774  nmfnge0t 9790  adjt 9796  adjeqt 9798  lnop0t 9829  nmlnop0ALT 9858  lnopm 9863  nmophm 9899  bdophm 9900  lnopcon 9901  lnfncon 9928  cnlnadjlem5 9942  cnlnadjeu 9948  nmoptri 9965  nmopcoadj 9972  unierr 9975  leoprf2t 9998  leopnmidt 10009  nmopleidt 10010  hmopidmch 10017  stelt 10079  hstelt 10080  hstle1t 10091  hstlest 10096  hst0t 10098  strlem3a 10117  strlem5 10120  strlem6 10121  hstrlem6 10129  jplem1 10133  dmdbr2 10168  mdslj1 10183  mdsl1 10185  mdsl2 10186  mdsl2b 10187  cvmd 10188  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd1 10193  mdslmd2 10194  csmdsym 10198  mdexch 10199  superpos 10218  atoml 10246  atoml2 10247  atord 10248  irredlem1 10254  irredlem2 10255  irredlem3 10256  irred 10258  atcvat4 10261  atabs 10265  mdsymlem1 10267  mdsymlem3 10269  mdsymlem5 10271  mdsymlem6 10272  sumdmdi 10278  sumdmdlem2 10282  dmdbr5at 10284  dmdbr6at 10285  mddmdin0 10292  cdj3lem1 10295  cdj3lem2 10296  elsymgrn 10335  oprabvaligg 10377  neiopne 10405  topnem 10430  mapdiscn 10434  efilcp 10481  efilcp2 10486  cnfilca 10487  emhgrat 10647

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