Theorem mpan2 519

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  mpan12 530  mp3an3 641  eueq2 1429  eueq3 1430  sbcgf 1469  ss0b 1726  nnullss 1880  unisseq 1946  ordeleqon 2241  ordsson 2242  ord0eln0 2278  ssnlim 2407  reldm0 2550  resieq 2581  ssres2 2590  resabs2 2593  iss 2599  resid 2601  coi2 2666  funcnvres 2710  fnresin1 2735  fnresin2 2736  fnf 2753  funbrfv 2852  dmfco 2864  fvco 2865  fvopab3 2868  fvopab3ig 2869  fvopab4 2871  fvopabn 2873  elrnopab 2884  fsn 2895  fsn2 2896  fconst2 2902  f1owe 2943  tfr3 2964  abianfplem 2999  oprabvalig 3048  1stval 3089  2ndval 3090  oa0 3124  om0 3125  oa1suc 3132  om1 3144  oe1 3146  oe1m 3147  nnarcl 3174  ecelqsi 3229  mapsn 3269  mapss 3270  2dom 3332  xpdom1 3346  pw2en 3348  sbthlem2 3350  sbthlem7 3355  mapdom1 3387  mapdom2 3389  mapxpen 3390  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  limensuci 3401  phplem5 3407  php 3409  infn0 3427  unblem1 3431  unblem2 3432  unblem3 3433  unblem4 3434  isfinite2 3437  unfilem1 3438  unfilem2 3439  unfi 3441  fiint 3445  inf0 3457  infensuc 3484  trcl 3489  r1suc 3496  rankr1lem 3517  ssrankr1 3520  rankr1a 3521  r1val2 3522  scott0 3542  ac5b 3574  ac6lem 3575  fodom 3613  fodomb 3615  cardval 3633  carden 3638  cardeq0 3639  carddomi 3641  unxpdomlem 3649  unxpdom2 3651  sucxpdom 3652  alephsuc 3672  alephnbtwn2 3675  alephsucdom 3685  alephle 3689  cardaleph 3690  iscard3 3693  cflem 3700  cflecard 3707  cdavalt 3716  cdaen 3719  cdadom1 3727  cdadom2 3728  cdafi 3730  cdainf 3731  mulidpi 3808  nlt1pi 3827  indpi 3828  1qec 3862  mulidpq 3863  1idpr 3927  prlem934a 3931  prlem934b 3932  prlem934 3933  0idsr 4000  1idsr 4001  00sr 4002  negexsr 4005  recexsrlem 4006  sqgt0sr 4009  map2psrpr 4014  supsrlem1 4019  supsrlem2 4020  addresr 4050  mulresr 4051  ax0id 4076  ax1id 4077  axcnre 4087  addcan 4120  negeu 4124  subadd 4143  mulcan 4207  receu 4215  divmul 4218  lt0neg1t 4370  le0neg1t 4372  recgt0i 4385  divgt0lem 4389  nnssre 4425  nnge1t 4439  nnleltp1t 4448  nnaddm1clt 4452  nominpos 4509  sup2 4510  nnunb 4520  lt0nnn0 4549  peano2nn0 4555  nn0ltp1let 4556  nn0ltlem1 4558  nn0lele2x 4563  elnnz 4572  elznn0 4576  elnnz1 4581  elnn0nn 4593  elnnnn0 4594  zltp1let 4597  zleltp1t 4598  zlem1ltt 4599  zneo 4601  peano2uz 4602  uzind 4603  uzwo 4605  uzwo2 4606  nnwoOLD 4608  zbtwnre 4619  rebtwnz 4620  flgzt 4626  znq 4630  qbtwnre 4650  om2uzsuc 4652  seqrn2 4674  exp1t 4679  exp2t 4683  sqreclt 4697  nneo 4719  nn0opthlem2 4723  sqrlem5 4735  sqrlem6 4736  sqrlem12 4742  sqrlem13 4743  sqrsq 4764  reim0 4809  leabs 4852  climunii 4883  ruclem13 4897  ruclem15 4899  ruclem28 4912  ruclem30 4914  xpnnen 4927  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  infmap2 4953  hvaddid2t 5003  hvmul0t 5004  hvsub0t 5041  hizer2t 5055  hlimunii 5143  occllem6 5185  projlem10 5202  projlem12 5204  projlem13 5205  projlem15 5207  projlem25 5217  projlem26 5218  pjthlem6 5230  pjthlem7 5231  pjthlem8 5232  pjthlem11 5235  omlsilem 5249  pjpj0 5259  pjoc1 5268  shsvat 5285  shsupunss 5316  chsupunss 5317  shmod 5364  chlejb1 5397  h1det 5455  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  spanunsn 5482  pjoml2 5495  osumlem4 5533  pjorth 5559  strlem6 5697  cvexchlem 5759  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdi 5785  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