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-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is referenced by:  mpanr12  666  mp3an23  1269  equs4  1959  eueq2  3011  sbcgf  3110  csbconstgf  3150  sbcnestg  3186  csbnestg  3187  csbnest1g  3189  eqpw1  4163  imakexg  4300  imagekexg  4312  setswith  4322  eqpw1uni  4331  sspw1  4336  finds  4412  nnc0suc  4413  elsuci  4415  lefinaddc  4451  nulge  4457  ltfinp1  4463  ncfinsn  4477  tfinltfinlem1  4501  sucevenodd  4511  sucoddeven  4512  oddtfin  4519  sfintfin  4533  vfinspnn  4542  1cvsfin  4543  tncveqnc1fin  4545  vfintle  4547  vfin1cltv  4548  vfinncvntnn  4549  vfinspsslem1  4551  vfinncsp  4555  vinf  4556  epelc  4766  xpss1  4857  br1st  4859  br2nd  4860  brswap2  4861  ssrnres  5060  rnexg  5105  resexg  5117  funcnvres  5166  fnresin1  5198  fnresin2  5199  fvopab3g  5387  fvopab4  5390  fsn  5433  fsn2  5435  f1elima  5475  mpteq1  5659  fvmpt  5701  fvmptnf  5724  fixexg  5789  ins3exg  5797  imageexg  5801  pprodexg  5838  clos1induct  5881  ecexg  5950  ecelqsg  5980  enmap2lem3  6066  enpw  6088  ncaddccl  6145  peano2nc  6146  ncdisjeq  6149  pw1eltc  6163  ovcelem1  6172  ce0nnul  6178  ce0nn  6181  ce0nulnc  6185  ce0  6191  lecidg  6197  lecncvg  6200  leconnnc  6219  ncfin  6248  nclenn  6250  ncslesuc  6268  nmembers1  6272  spaccl  6287  nchoicelem3  6292  nchoicelem9  6298  nchoicelem19  6308  frecxpg  6316  fnfreclem1  6318  fnfreclem3  6320  scancan  6332