Theorem mpan2 696

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 707  mp3an3 905  mp3an23 908  a12lem1 1376  euor2 1437  eueq2 1918  eueq3 1919  sbccomg 1989  sbcralg 1994  sbcrexg 1995  unimax 2532  nnullss 2768  eldifpw 2910  ordeleqon 2990  ordsson 2991  ord0eln0 3023  ssnlim 3167  reldm0 3331  ssres2 3386  resdm 3393  iss 3397  resid 3400  ssrnres 3481  coi2 3511  funcnvres 3568  funimaex 3576  isarep1 3577  fnresin1 3601  fnresin2 3602  fnf 3628  funssxp 3638  funbrfv 3750  ssimaex 3768  dmfco 3773  fvco 3774  fvopab3 3777  fvopab3ig 3778  fvopab4 3780  fvopab4sf 3782  fvopabn 3786  fvimacnvALT 3809  dff4 3816  dff2 3817  rnssopab 3825  fopabco 3832  fopabcos 3833  fsn 3834  fsn2 3836  fopabsn 3840  f1owe 3905  tfr3 3926  abianfplem 3961  abianfp 3962  oprabvalig 4024  oprabval2gf 4026  1stval 4081  2ndval 4082  2ndconst 4097  curry1 4098  eqop 4104  oa0 4155  om0 4156  oa1suc 4164  om1 4176  oe1 4178  oe1m 4179  oarec 4196  omass 4211  nnarcl 4232  nneob 4255  ecelqsi 4292  mapval2 4335  mapsn 4345  mapss 4346  2dom 4427  xpdom1 4443  pw2en 4446  sbthlem2 4448  sbthlem7 4453  fodomr 4483  mapdom1 4492  mapdom2 4494  mapxpen 4495  xpmapenlem2 4497  xpmapenlem4 4499  xpmapenlem5 4500  mapunen 4502  limensuci 4506  phplem4 4511  php 4513  infn0 4533  unblem1 4540  unblem2 4541  unblem3 4542  unblem4 4543  isfinite2OLD 4546  unfilem1 4548  unfilem2 4549  unfi 4551  unfiOLD 4552  unifiOLD 4557  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  pwfilemOLD 4570  pm54.43 4572  inf0 4606  infensuc 4638  trcl 4645  r1suc 4652  rankr1lem 4673  ssrankr1 4676  rankr1a 4677  rankxplim3 4714  scott0 4717  ac5b 4753  ac6lem 4754  fodom 4798  brdom3 4801  brdom5 4802  brdom4 4803  iundom 4812  cardval 4826  carden 4831  cardeq0 4832  card1 4833  carddomi 4835  unxpdomlem 4843  unxpdom2 4845  sucxpdom 4846  alephsuc 4866  alephnbtwn2 4869  alephsucdom 4880  alephle 4884  cardaleph 4885  iscard3 4888  alephfplem2 4897  alephfp 4900  cflem 4905  cflecard 4912  cfeq0 4914  cdavalt 4919  cdaen 4924  cdadom1 4933  cdadom2 4934  cdafi 4936  cdainf 4937  mulidpi 5014  nlt1pi 5033  indpi 5034  mulidpq 5069  1idpr 5133  prlem934a 5137  prlem934b 5138  prlem934 5139  0idsr 5206  1idsr 5207  00sr 5208  negexsr 5211  recexsrlem 5212  sqgt0sr 5215  map2psrpr 5220  supsrlem1 5225  supsrlem2 5226  addresr 5256  mulresr 5257  ax0id 5281  ax1id 5282  axcnre 5286  peano2cn 5344  addcan 5351  negeu 5355  subadd 5371  negidt 5379  peano2re 5436  peano2rem 5442  renepnft 5537  renemnft 5538  ltpnft 5542  nltmnft 5547  pnfget 5548  nltpnftt 5566  ne0gt0t 5619  lt0neg1t 5668  le0neg1t 5670  mulcan 5686  mulcanOLD 5687  receu 5701  divmul 5705  recgt0i 5814  divgt0i2 5859  reclt1t 5898  recp1lt1 5901  recrecltt 5902  ledivp1 5906  ltdivp1 5907  nnge1t 5943  nnle1eq1t 5945  lt1nnn 5947  nnleltp1t 5954  times2t 6005  halfpm6th 6032  halfaddsubt 6041  nominpos 6043  avglet 6044  lbinfm 6048  supxrbnd 6091  supxrgtmnf 6092  supxrre1 6093  supxrre2 6094  nn0le0eq0t 6119  peano2nn0 6124  nn0ltp1let 6127  nn0ltlem1t 6129  nn0lele2x 6135  elnnz 6145  elznn0 6149  elnnz1 6155  znnnlt1t 6156  peano2z 6166  peano2zm 6169  elnnnn0 6172  zltp1let 6181  zlem1ltt 6183  zltlem1t 6184  zeot 6199  zneo 6200  dfuz 6202  uzindOLD 6208  uzwo4OLD 6210  uzwo5OLD 6211  rebtwnz 6222  flge0nn0t 6242  flge1nnt 6243  btwnzge0t 6245  flhalft 6246  ceim1lt 6249  qbtwnre 6278  qsqueeze 6280  monoord 6294  om2uzsuc 6296  seq1m1 6319  seq1rn 6322  ser1ft 6328  icoshftf1oi 6409  icounlem 6412  eluzaddi 6436  eluzsubi 6437  peano2uzr 6448  uzwo 6455  uzwoOLD 6456  uzwo2 6457  infmssuzle 6465  infmssuzcl 6466  limsupvalt 6529  seqzfval 6537  seq1seq02t 6543  seqz1 6547  seqzp1 6548  seqzm1 6549  seq0p1 6551  seqzval2t 6553  seqzresval 6559  seqzres 6560  seqzres2 6561  exp0t 6571  exp1t 6573  expm1t 6583  expword2it 6605  expubndt 6608  sqvalt 6609  sqeq0t 6613  resqclt 6621  sumsqne0 6634  expnbndt 6654  nn0opthlem2 6665  sqrlem5 6677  sqrlem6 6678  sqrlem13 6685  sqrmsq2 6706  imcjt 6819  cjne0t 6831  leabs 6872  abs2dift 6902  facnn2t 6939  facndivt 6943  faclbnd2 6946  faclbnd4lem1 6948  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd5 6953  bcval4t 6961  bcnp11t 6965  bcnp1nt 6966  sumeq2 6985  sumeqfv 6997  dffsum 6998  serzfsum 7004  fsump1 7006  fsum4 7025  csbfsumlem 7026  fsum0 7039  ser1ser0 7048  serzref 7051  serz0 7053  serzsplit 7056  serzmulc 7058  serzrelem 7061  binomlem2 7067  bcxmas 7076  climfnn 7092  climunii 7098  climshft 7104  climshft2 7106  iserzshft2 7107  climge0 7112  climaddlem3 7116  clim2serz 7145  climserzle 7147  climabslem 7148  climubi 7153  climsup 7155  climcau 7156  caucvg 7163  caucvg3lem 7166  serzf0 7169  ser1f0 7170  iserzabslem 7178  cvgcmp2lem 7180  isumval2t 7194  isumclim3t 7200  infcvgaux2 7220  infcvglem1 7221  fnsmnt 7226  expcnvlem2 7228  geoser 7234  geolimilem 7235  geoisumr 7243  geoisum1c 7245  cvgratlem1ALT 7247  fsum0diaglem1 7256  fsum0diag2 7259  fsum0diag4 7261  ivthlem6 7286  ivthlem7 7287  dsupivthlem 7291  efseq0ex 7311  erelem3 7321  efaddlem1 7338  efaddlem15 7352  efaddlem16 7353  efaddlem20 7357  efaddlem26 7363  efaddlem27 7364  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem1 7389  eirrlem3 7391  eirrlem4 7392  efgt0 7404  eflegeolem2 7414  efcnlem1 7419  efcnlem2 7420  reeff1o 7426  efi4pt 7435  resin4pt 7436  recos4pt 7437  efivalt 7447  sinbndt 7465  cosbndt 7466  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  cos01bndlem3 7471  cos2bnd 7475  sin01gt0 7476  cos01gt0 7477  sin02gt0 7478  sin4lt0 7481  xpnnen 7499  znnenlem 7501  znnen 7502  unben 7505  ruclem15 7524  ruclem28 7537  ruclem30 7539  infxpidmlem1 7552  infxpidmlem11 7562  infxpidmlem12 7563  infdif 7568  infpss 7574  infmap2 7581  0opnt 7601  topopn 7602  tgvalt 7616  unitgt 7623  sn0top 7647  fctopOLD 7650  cctop 7652  isopn2 7673  0cld 7678  iincld 7679  ntropn 7684  ntrval2 7686  cmclsopn 7693  cmntrcld 7694  clstop 7700  ntrtop 7701  cls0 7709  ntr0 7710  neiint 7719  neips 7727  cncnplem4 7777  cnconst 7780  metres 7823  metxp 7834  blfval 7835  bl2in 7843  blex 7849  opnm 7860  ioo2bl 7912  lmbrf 7930  lmnn 7935  iscauf 7939  iscau5 7941  iscaunns 7944  lmsslem 7952  lmss 7953  caussi 7954  causs 7955  lmclimnn 7964  metcn4i 7972  oprcn 7977  fsumcnlem 7989  iscms2lem4 7992  lmcau 7996  bcthlem1 7999  bcthlem16 8014  bcthlem21 8019  cnid 8127  mulid 8132  vcoprne 8198  bafval 8223  invfval 8261  nvnd 8319  ipfval 8352  ipval2lem3 8355  ipval2 8357  ipval2lem6 8361  4ipval3 8362  ipid 8363  ipcj 8367  ip0r 8370  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem4 8376  islno 8414  lno0 8417  nmoge0 8430  nmlno0lem 8453  nmlnogt0 8457  blocni 8465  ipasslem2 8491  ipasslem8 8497  ipasslem9 8498  ipasslem11 8500  ubthlem6 8534  minveclem24 8568  minveclem25 8569  minveclem26 8570  minveclem27 8571  minveclem28 8572  minveclem32 8576  minveclem38 8582  minveceu 8583  pilem1 8671  pilem2 8672  sinhalfpilem 8679  sinperlem1 8686  sinper 8690  cosper 8691  sin2pim 8692  cos2pim 8693  sinmpi 8694  cosmpi 8695  sinppi 8696  sinkpi 8697  efimpi 8698  sincosq1lem 8703  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  sinq12gt0t 8708  sincosq1eq 8709  sincos4thpi 8710  sincos6thpi 8711  abssinper 8712  sineq0 8713  cosh111lem1 8714  efifolem4 8725  efifolem5 8726  efifolem6 8727  efifolem7 8728  efif1lem1 8730  efif1lem2 8731  shftefif1olem 8741  efper 8747  h2hcau 8849  h2hlm 8850  hvaddid2t 8892  hvsubcant 8941  hvsubcan2t 8942  hvsub0t 8943  hi02t 8963  hilid 9028  hcau 9051  hlim2 9060  chlim 9104  hlimunii 9108  hhsscms 9150  projlem10 9195  projlem12 9197  projlem13 9198  projlem15 9200  projlem25 9210  projlem26 9211  pjthlem7 9225  pjthlem8 9226  pjthlem11 9229  omlsilem 9244  pjpj0 9255  pjoc1 9264  shsupunss 9315  chsupunss 9316  shmod 9363  chlejb1 9399  h1det 9473  h1de2b 9477  h1de2ctlem 9478  h1de2ct 9479  spanunsn 9502  pjoml2 9528  osumlem4 9581  pjorth 9614  mayete3 9673  hosubid1t 9724  elcnopt 9783  ellnopt 9784  nmoprepnf 9794  elunopt 9799  elhmopt 9800  nmfnrepnf 9807  elcnfnt 9809  ellnfnt 9810  adjvalt 9814  nmopge0t 9835  nmfnge0t 9851  adjt 9857  adjeqt 9859  lnop0t 9890  nmlnop0ALT 9920  lnopm 9925  nmophm 9961  bdophm 9962  lnopcon 9963  lnfncon 9990  cnlnadjlem5 10004  cnlnadjeu 10010  nmoptri 10027  nmopcoadj 10034  unierr 10037  leoprf2t 10060  leopnmidt 10071  nmopleidt 10072  hmopidmch 10079  stelt 10141  hstelt 10142  hstle1t 10153  hstlest 10158  hst0t 10160  strlem3a 10179  strlem5 10182  hstrlem6 10191  jplem1 10195  dmdbr2 10230  mdslj1 10246  mdsl1 10248  mdsl2 10249  mdsl2b 10250  cvmd 10251  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd1 10256  mdslmd2 10257  csmdsym 10261  mdexch 10262  superpos 10281  atoml 10309  atoml2 10310  atord 10311  irredlem1 10317  irredlem2 10318  irredlem3 10319  irred 10321  atcvat4 10324  atabs 10328  mdsymlem1 10330  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  sumdmdi 10342  sumdmdlem2 10346  dmdbr5at 10349  dmdbr6at 10350  mddmdin0 10358  cdj3lem1 10361  cdj3lem2 10362  elsymgrn 10401  oprabvaligg 10440  neiopne 10474  topnem 10507  mapdiscn 10511  top2ind 10548  top2usne 10549  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596  emhgrat 10775

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