Theorem mpan 518

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpan.1	|- ph
mpan.2	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mpan	|- (ps -> ch)

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. 2 |- ph
2		mpan.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	exp 291	. 2 |- (ph -> (ps -> ch))
4	1, 3	ax-mp 6	1 |- (ps -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  mp2an 520  mpan11 529  mp3an1 639  elssuni 1940  opeluu 1953  unipw 1960  supmo 2156  supsn 2168  fr2nr 2177  fr3nr 2178  tfi 2244  onint 2261  onminsb 2264  onminesb 2265  onintrab 2268  onnminsb 2271  onminex 2275  onel 2346  onuninsuc 2356  on0eqelt 2370  dfom2 2374  peano5 2394  tfindsg2 2403  brrelexi 2447  relsn 2485  soirri 2629  sotri 2630  dfrel2 2660  coi1 2665  fssxp 2761  fssres 2764  fcoi1 2765  fcoi2 2766  fvopab3 2868  fconst2 2902  tfrlem10 2958  rdgsucopab 2984  rdglim2 2987  frsucopab 2992  tz7.48lem 2993  tz7.48-1 2994  tz7.48-2 2995  tz7.49 2997  tz7.49c 2998  abianfplem 2999  abianfp 3000  oprabval 3047  ndmopr 3059  ordgt0ge1 3114  oe0m 3127  oa0r 3141  om0r 3142  om1r 3145  oe1m 3147  oawordeulem 3156  oaass 3163  oen0 3165  map0 3268  ssdomg 3311  snfi 3337  undom 3342  xpdom1 3346  xpdom3 3347  mapdom2 3389  pwen 3398  limenpsi 3400  limensuci 3401  php 3409  onomeneq 3414  0sdom1dom 3420  omsdomnn 3424  unblem1 3431  unblem4 3434  unfilem1 3438  opthreg 3455  inf0 3457  infensuc 3484  r1tr 3498  r1ord 3499  tz9.12lem1 3503  tz9.12lem3 3505  tz9.12 3506  rankon 3515  rankr1lem 3517  rankval3 3525  bndrank 3526  unbndrank 3527  ranklon 3540  scott0 3542  karden 3551  numth2 3600  numthcor 3601  zornlem2 3604  zornlem4 3606  zornlem5 3607  zorn2 3612  oncardval 3626  oncardon 3627  oncardid 3628  oncard 3636  cardne 3637  carden 3638  sucdom 3648  unxpdom2 3651  sucxpdom 3652  cardcard 3655  cardsdomel 3658  carduni 3664  cardmin 3666  cardprc 3667  alephon 3671  alephcard 3673  alephordi 3679  alephgeom 3687  alephprc 3698  cardcf 3706  cdacomen 3724  cdadom2 3728  indpi 3828  ltsopq 3869  ltrpq 3879  prub 3892  genpnnp 3902  distrlem4pr 3924  prlem934b 3932  ltapr 3945  addcanpr 3946  suplem2pr 3956  ltsosr 3997  sqgt0sr 4009  mappsrpr 4012  suppsr2 4017  suppsr3 4018  supsrlem1 4019  ltsor 4055  axmulcl 4068  axmulass 4073  axdistr 4074  axlttri 4083  axlttrn 4084  addcan 4120  addid2t 4132  negclt 4141  renegcl 4171  mulid2t 4175  mulzer2t 4189  mulm1t 4204  mulcan 4207  mul0or 4210  divassz 4241  divdiv23z 4273  lttri2t 4280  lttri3t 4281  ltnrt 4292  lt0neg2t 4371  le0neg2t 4373  ltplus1t 4383  lemul2 4396  posex 4422  nnge1t 4439  nngt1ne1t 4440  nngt0t 4441  lt1nnn 4442  nnrecgt0t 4447  nnsub 4450  nnaddm1clt 4452  suprubi 4517  nnunb 4520  rimul 4534  nn0ge0t 4550  elnnz 4572  elnn0z 4574  elnnz1 4581  elnn0nn 4593  zltp1let 4597  zneo 4601  nnwo 4607  zqt 4632  nnrecqt 4649  om2uzuz 4653  om2uzran 4655  uzrdgval 4657  uzrdgsuc 4659  seqlem2 4663  seqrn 4673  0expt 4680  1expt 4681  discrlem2 4714  discrlem3 4715  nnesq 4720  sqrlem5 4735  sqrlem6 4736  sqrlem12 4742  sqrlem16 4746  sqrlem17 4747  sqrge0 4760  sqrsqid 4766  reim0 4809  abslt 4855  absle 4856  abs3lem 4861  clim0 4882  climunii 4883  ruclem13 4897  ruclem15 4899  ruclem28 4912  ruclem31 4915  nn0ennn 4925  znnenlem 4929  znnen 4930  infxpidmlem10 4942  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  infmap1 4950  infmap2 4953  alephexp1 4954  alephexp2 4956  gch-kn 4957  hvsubclt 4998  hvsubidt 5005  hvsub4t 5014  hvaddsub12t 5015  hvsubcan1t 5016  hvaddsubasst 5018  his2subt 5052  hizer1t 5054  norm3lem 5096  hlim0 5140  hlimcaui 5141  hlimunii 5143  projlem6 5198  pjthlem2 5226  pjthlem3 5227  pjthlem7 5231  pjthlem8 5232  pjthu 5241  pjthu2 5242  omlsi 5250  pjcl 5255  pjhcl 5256  pjoml 5271  ococint 5298  spanvalt 5300  spanclt 5305  shlub 5347  shslub 5359  h1de2ctlem 5460  spanunsn 5482  pjoml5 5498  osumlem7 5536  spansncv 5542  pjch0t 5562  pjcomp 5565  pjocin 5583  pjin 5584  pjjs 5585  pjrn 5587  pjv 5589  pjsumt 5590  hocl 5594  hoscl 5596  hodcl 5597  hoco 5598  hoscom 5605  hods 5606  hosass 5607  hosdir 5609  hoddir 5610  hoid0 5614  pjsdi 5625  pjddi 5626  pjss1co 5633  pjscj 5640  pjtot 5644  pjclem4a 5652  pj3lem1 5658  pj3s 5659  pjs14 5669  strlem4 5695  strlem5 5696  jplem1 5701  elat2 5739  shatomic 5753  chrelat 5757  chrelat2 5758  cvexchlem 5759  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdlem 5786  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org