Theorem mpan2 652

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

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	. . 3 |- ps
2	1	a1i 10	. 2 |- (ph -> ps)
3		mpan2.2	. 2 |- ((ph /\ ps) -> ch)
4	2, 3	mpdan 649	1 |- (ph -> ch)

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mpanr12  666  mp3an23  1269  equs4  1959  eueq2  3010  sbcgf  3109  csbconstgf  3149  sbcnestg  3185  csbnestg  3186  csbnest1g  3188  eqpw1  4162  imakexg  4299  imagekexg  4311  setswith  4321  eqpw1uni  4330  sspw1  4335  finds  4411  nnc0suc  4412  elsuci  4414  lefinaddc  4450  nulge  4456  ltfinp1  4462  ncfinsn  4476  tfinltfinlem1  4500  sucevenodd  4510  sucoddeven  4511  oddtfin  4518  sfintfin  4532  vfinspnn  4541  1cvsfin  4542  tncveqnc1fin  4544  vfintle  4546  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  vfinncsp  4554  vinf  4555  epelc  4765  xpss1  4856  br1st  4858  br2nd  4859  brswap2  4860  ssrnres  5059  rnexg  5104  resexg  5116  funcnvres  5165  fnresin1  5197  fnresin2  5198  fvopab3g  5386  fvopab4  5389  fsn  5432  fsn2  5434  f1elima  5474  mpteq1  5658  fvmpt  5700  fvmptnf  5723  fixexg  5788  ins3exg  5796  imageexg  5800  pprodexg  5837  clos1induct  5880  ecexg  5949  ecelqsg  5979  enmap2lem3  6065  enpw  6087  ncaddccl  6144  peano2nc  6145  ncdisjeq  6148  pw1eltc  6162  ovcelem1  6171  ce0nnul  6177  ce0nn  6180  ce0nulnc  6184  ce0  6190  lecidg  6196  lecncvg  6199  leconnnc  6218  ncfin  6247  nclenn  6249  ncslesuc  6267  nmembers1  6271  spaccl  6286  nchoicelem3  6291  nchoicelem9  6297  nchoicelem19  6307  frecxpg  6315  fnfreclem1  6317  fnfreclem3  6319  scancan  6331