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 904  mp3an23 907  a12lem1 1375  euor2 1436  eueq2 1915  eueq3 1916  sbccomg 1986  sbcralg 1991  sbcrexg 1992  unimax 2528  nnullss 2764  eldifpw 2906  ordeleqon 2986  ordsson 2987  ord0eln0 3019  ssnlim 3163  reldm0 3327  ssres2 3382  resdm 3389  iss 3393  resid 3396  ssrnres 3477  coi2 3507  funcnvres 3564  funimaex 3572  isarep1 3573  fnresin1 3597  fnresin2 3598  fnf 3624  funssxp 3633  funbrfv 3745  ssimaex 3763  dmfco 3768  fvco 3769  fvopab3 3772  fvopab3ig 3773  fvopab4 3775  fvopab4sf 3777  fvopabn 3781  fvimacnvALT 3804  dff4 3811  dff2 3812  rnssopab 3820  fopabco 3827  fopabcos 3828  fsn 3829  fsn2 3831  fopabsn 3835  f1owe 3900  tfr3 3921  abianfplem 3956  abianfp 3957  oprabvalig 4019  oprabval2gf 4021  1stval 4074  2ndval 4075  2ndconst 4090  curry1 4091  eqop 4097  oa0 4148  om0 4149  oa1suc 4157  om1 4169  oe1 4171  oe1m 4172  oarec 4189  omass 4204  nnarcl 4225  nneob 4248  ecelqsi 4285  mapval2 4328  mapsn 4338  mapss 4339  2dom 4417  xpdom1 4432  pw2en 4435  sbthlem2 4437  sbthlem7 4442  fodomr 4472  mapdom1 4481  mapdom2 4483  mapxpen 4484  xpmapenlem2 4486  xpmapenlem4 4488  xpmapenlem5 4489  mapunen 4491  limensuci 4495  phplem4 4500  php 4502  infn0 4521  unblem1 4526  unblem2 4527  unblem3 4528  unblem4 4529  isfinite2 4532  unfilem1 4533  unfilem2 4534  unfi 4537  unifi 4541  fiint 4543  fodomfi 4549  pwfilem 4553  pm54.43 4555  inf0 4589  infensuc 4621  trcl 4628  r1suc 4635  rankr1lem 4656  ssrankr1 4659  rankr1a 4660  rankxplim3 4697  scott0 4700  ac5b 4736  ac6lem 4737  fodom 4781  brdom3 4784  brdom5 4785  brdom4 4786  iundom 4795  cardval 4809  carden 4814  cardeq0 4815  card1 4816  carddomi 4818  unxpdomlem 4826  unxpdom2 4828  sucxpdom 4829  alephsuc 4849  alephnbtwn2 4852  alephsucdom 4863  alephle 4867  cardaleph 4868  iscard3 4871  alephfplem2 4880  alephfp 4883  cflem 4888  cflecard 4895  cfeq0 4897  cdavalt 4902  cdaen 4907  cdadom1 4916  cdadom2 4917  cdafi 4919  cdainf 4920  mulidpi 4997  nlt1pi 5016  indpi 5017  mulidpq 5052  1idpr 5116  prlem934a 5120  prlem934b 5121  prlem934 5122  0idsr 5189  1idsr 5190  00sr 5191  negexsr 5194  recexsrlem 5195  sqgt0sr 5198  map2psrpr 5203  supsrlem1 5208  supsrlem2 5209  addresr 5239  mulresr 5240  ax0id 5264  ax1id 5265  axcnre 5269  peano2cn 5327  addcan 5334  negeu 5338  subadd 5354  negidt 5362  peano2re 5419  peano2rem 5425  renepnft 5520  renemnft 5521  ltpnft 5525  nltmnft 5530  pnfget 5531  nltpnftt 5549  ne0gt0t 5603  lt0neg1t 5651  le0neg1t 5653  mulcan 5669  receu 5680  divmul 5684  recgt0i 5780  divgt0i2 5823  reclt1t 5856  recp1lt1 5859  recrecltt 5860  ledivp1 5864  ltdivp1 5865  nnge1t 5901  nnle1eq1t 5903  lt1nnn 5905  nnleltp1t 5911  times2t 5962  halfpm6th 5989  2halvest 5996  halfaddsubt 5998  nominpos 6000  avglet 6001  lbinfm 6005  supxrbnd 6048  supxrgtmnf 6049  supxrre1 6050  supxrre2 6051  nn0le0eq0t 6076  peano2nn0 6081  nn0ltp1let 6084  nn0ltlem1t 6086  nn0lele2x 6092  elnnz 6102  elznn0 6106  elnnz1 6112  znnnlt1t 6113  peano2z 6123  peano2zm 6126  elnnnn0 6129  zltp1let 6138  zlem1ltt 6140  zltlem1t 6141  nneo 6154  zeot 6156  zneo 6157  zneoOLD 6158  dfuz 6160  uzindOLD 6166  uzwo4OLD 6168  uzwo5OLD 6169  rebtwnz 6180  flge0nn0t 6197  flge1nnt 6198  btwnzge0t 6200  flhalft 6201  ceim1lt 6204  qbtwnre 6228  qsqueeze 6230  monoord 6244  om2uzsuc 6246  seq1m1 6269  seq1rn 6272  ser1ft 6278  icoshftf1oi 6355  icounlem 6358  eluzaddi 6381  eluzsubi 6382  peano2uzr 6393  uzwo 6400  uzwoOLD 6401  uzwo2 6402  infmssuzle 6410  infmssuzcl 6411  limsupvalt 6474  seqzfval 6482  seq1seq02t 6488  seqz1 6492  seqzp1 6493  seqzm1 6494  seq0p1 6496  seqzval2t 6498  seqzresval 6504  seqzres 6505  seqzres2 6506  exp0t 6516  exp1t 6518  expm1t 6528  expword2it 6550  expubndt 6553  sqvalt 6554  sqeq0t 6558  resqclt 6566  sumsqne0 6579  expnbndt 6599  nn0opthlem2 6610  sqrlem5 6622  sqrlem6 6623  sqrlem13 6630  sqrmsq2 6651  crutOLD 6684  crretOLD 6718  crimtOLD 6720  imret 6725  recjt 6768  imcjt 6769  cjne0t 6781  leabs 6822  abs2dift 6854  facnn2t 6891  facndivt 6895  faclbnd2 6898  faclbnd4lem1 6900  faclbnd4lem3 6902  faclbnd4lem4 6903  faclbnd5 6905  bcval4t 6914  bcnp11t 6918  bcnp1nt 6919  sumeq2 6938  sumeqfv 6950  dffsum 6951  serzfsum 6957  fsump1 6959  fsum4 6978  csbfsumlem 6979  fsum0 6992  ser1ser0 7001  serzref 7004  serz0 7006  serzsplit 7009  serzmulc 7011  serzrelem 7014  binomlem2 7020  bcxmas 7029  climfnn 7045  climunii 7051  climshft 7057  climshft2 7059  iserzshft2 7060  climge0 7065  climaddlem3 7069  clim2serz 7098  climserzle 7100  climabslem 7101  climubi 7106  climsup 7108  climcau 7109  caucvg 7116  caucvg3lem 7119  serzf0 7122  ser1f0 7123  iserzabslem 7131  cvgcmp2lem 7133  isumval2t 7147  isumclim3t 7152  infcvgaux2 7172  infcvglem1 7173  fnsmnt 7178  expcnvlem2 7180  geoser 7186  geolimilem 7187  geoisumr 7195  geoisum1c 7197  cvgratlem1ALT 7199  fsum0diaglem1 7208  fsum0diag2 7211  fsum0diag4 7213  ivthlem6 7238  ivthlem7 7239  dsupivthlem 7243  ivthlem6OLD 7247  ivthlem7OLD 7248  efseq0ex 7270  erelem3 7280  efaddlem1 7297  efaddlem15 7311  efaddlem16 7312  efaddlem20 7316  efaddlem26 7322  efaddlem27 7323  ef01tllem1 7342  ef01tllem2 7343  absef01tllem 7345  eirrlem1 7347  eirrlem3 7349  eirrlem4 7350  efgt0 7362  eflegeolem2 7371  efcnlem1 7376  efcnlem2 7377  reeff1o 7385  efi4pt 7394  resin4pt 7395  recos4pt 7396  efivalt 7406  sinbndt 7424  cosbndt 7425  sin01bndlem2 7427  sin01bndlem3 7428  cos01bndlem2 7429  cos01bndlem3 7430  cos2bnd 7434  sin01gt0 7435  cos01gt0 7436  sin02gt0 7437  sin4lt0 7440  xpnnen 7458  znnenlem 7460  znnenlemOLD 7461  znnen 7462  unben 7465  ruclem15 7484  ruclem28 7497  ruclem30 7499  infxpidmlem1 7512  infxpidmlem11 7522  infxpidmlem12 7523  infdif 7528  infpss 7534  infmap2 7541  0opnt 7561  topopn 7562  tgvalt 7576  unitgt 7583  sn0top 7607  fctop 7610  cctop 7612  isopn2 7633  0cld 7638  iincld 7639  ntropn 7644  ntrval2 7646  cmclsopn 7653  cmntrcld 7654  clstop 7660  ntrtop 7661  cls0 7669  ntr0 7670  neiint 7679  neips 7687  cncnplem4 7737  cnconst 7740  metres 7785  metxp 7796  blfval 7797  bl2in 7805  blex 7811  opnm 7822  ioo2bl 7874  lmbrf 7892  lmnn 7897  iscauf 7901  iscau5 7903  iscaunns 7906  lmsslem 7914  lmss 7915  caussi 7916  causs 7917  lmclimnn 7926  metcn4i 7934  oprcn 7939  fsumcnlem 7951  iscms2lem4 7954  lmcau 7958  bcthlem1 7961  bcthlem16 7976  bcthlem21 7981  cnid 8091  mulid 8096  vcoprne 8162  bafval 8187  invfval 8225  nvnd 8283  ipfval 8314  ipval2lem3 8317  ipval2 8319  ipval2lem6 8323  4ipval3 8324  ipid 8325  ipcj 8329  ip0r 8332  ip1cnilem2 8336  ip1cnilem3 8337  ip1cnilem4 8338  islno 8376  lno0 8379  nmoge0 8390  nmlno0lem 8413  nmlnogt0 8417  blocni 8424  ipasslem2 8450  ipasslem8 8456  ipasslem9 8457  ipasslem11 8459  ubthlem6 8493  minveclem24 8527  minveclem25 8528  minveclem26 8529  minveclem27 8530  minveclem28 8531  minveclem32 8535  minveclem38 8541  minveceu 8542  pilem1 8625  pilem2 8626  sinhalfpilem 8633  sinperlem1 8640  sinper 8644  cosper 8645  sin2pim 8646  cos2pim 8647  sinmpi 8648  cosmpi 8649  efimpi 8650  sincosq1lem 8655  sincosq2sgn 8657  sincosq3sgn 8658  sincosq4sgn 8659  sinq12gt0t 8660  sincosq1eq 8661  sincos4thpi 8662  sincos6thpi 8663  cosh111lem1 8664  efifolem4 8675  efifolem5 8676  efifolem6 8677  efifolem7 8678  efif1lem1 8680  efif1lem2 8681  shftefif1olem 8696  efper 8702  h2hcau 8804  h2hlm 8805  hvaddid2t 8847  hvsubcant 8896  hvsubcan2t 8897  hvsub0t 8898  hi02t 8918  hilid 8983  hcau 9006  hlim2 9015  chlim 9059  hlimunii 9063  hhsscms 9105  projlem10 9150  projlem12 9152  projlem13 9153  projlem15 9155  projlem25 9165  projlem26 9166  pjthlem7 9180  pjthlem8 9181  pjthlem11 9184  omlsilem 9199  pjpj0 9210  pjoc1 9219  shsupunss 9270  chsupunss 9271  shmod 9318  chlejb1 9354  h1det 9428  h1de2b 9432  h1de2bOLD 9433  h1de2ctlem 9434  h1de2ct 9435  spanunsn 9459  pjoml2 9485  osumlem4 9538  pjorth 9571  mayete3 9630  hosubid1t 9681  elcnopt 9740  ellnopt 9741  nmoprepnf 9751  elunopt 9756  elhmopt 9757  nmfnrepnf 9764  elcnfnt 9766  ellnfnt 9767  adjvalt 9771  nmopge0t 9792  nmfnge0t 9808  adjt 9814  adjeqt 9816  lnop0t 9847  nmlnop0ALT 9876  lnopm 9881  nmophm 9917  bdophm 9918  lnopcon 9919  lnfncon 9946  cnlnadjlem5 9960  cnlnadjeu 9966  nmoptri 9983  nmopcoadj 9990  unierr 9993  leoprf2t 10016  leopnmidt 10027  nmopleidt 10028  hmopidmch 10035  stelt 10097  hstelt 10098  hstle1t 10109  hstlest 10114  hst0t 10116  strlem3a 10135  strlem5 10138  hstrlem6 10147  jplem1 10151  dmdbr2 10186  mdslj1 10202  mdsl1 10204  mdsl2 10205  mdsl2b 10206  cvmd 10207  mdslmd1lem1 10208  mdslmd1lem2 10209  mdslmd1 10212  mdslmd2 10213  csmdsym 10217  mdexch 10218  superpos 10237  atoml 10265  atoml2 10266  atord 10267  irredlem1 10273  irredlem2 10274  irredlem3 10275  irred 10277  atcvat4 10280  atabs 10284  mdsymlem1 10286  mdsymlem3 10288  mdsymlem5 10290  mdsymlem6 10291  sumdmdi 10298  sumdmdlem2 10302  dmdbr5at 10305  dmdbr6at 10306  mddmdin0 10314  cdj3lem1 10317  cdj3lem2 10318  elsymgrn 10357  oprabvaligg 10399  neiopne 10427  topnem 10453  mapdiscn 10457  efilcp 10504  efilcp2 10509  cnfilca 10510  rcfpfillem6 10516  emhgrat 10684

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