Theorem mpan 651

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

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	. . 3 |- ph
2	1	a1i 10	. 2 |- (ps -> ph)
3		mpan.2	. 2 |- ((ph /\ ps) -> ch)
4	2, 3	mpancom 650	1 |- (ps -> 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:  mp2an  653  mpanl12  663  mp3an1  1264  mp3an12  1267  mp3an13  1268  csbex  3148  sbnfc2  3197  ssdifss  3398  uneqdifeq  3639  elssuni  3920  riinrab  4042  opkelcokg  4262  elssetkg  4270  opkelimagekg  4272  uni1exg  4293  imagekexg  4312  uniexg  4317  intexg  4320  addcexg  4394  peano5  4410  0cminle  4462  spfininduct  4541  vfinspss  4552  phiexg  4572  opexg  4588  proj1exg  4592  proj2exg  4593  copsexg  4608  imaexg  4747  siexg  4753  opeliunxp  4821  xpss2  4858  cnvexg  5102  xpexg  5115  fco  5232  fssres  5239  fvopab3g  5387  ffvelrni  5417  fvconst2  5454  oprabid  5551  caovcl  5624  caovass  5628  caovdi  5635  txpexg  5785  ins2exg  5796  imageexg  5801  txpcofun  5804  fullfunexg  5860  fvfullfun  5865  brfullfung  5866  ecelqsi  5981  ectocl  5993  pmex  6006  map0  6026  f1oen  6034  enrflxg  6035  cnven  6046  xpsnen2g  6055  enmap2lem3  6066  enmap1lem3  6072  enprmaplem5  6081  nenpw1pwlem1  6085  nulnnc  6119  ovmuc  6131  ovcelem1  6172  lec0cg  6199  sbthlem1  6204  nc0suc  6218  dflec3  6222  letc  6232  ce2t  6236  muc0or  6253  nchoicelem9  6298  nchoicelem17  6306  frecexg  6313  frecxp  6315  dmfrec  6317