Theorem mpanl12 436

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mpanl12.1	|- ph
mpanl12.2	|- ps
mpanl12.3	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
mpanl12	|- ( ch -> th )

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 |- ps
2		mpanl12.1	. . 3 |- ph
3		mpanl12.3	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	mpanl1 434	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  reuun1  3507  ordtri2orexmid  4650  opthreg  4683  ordtri2or2exmid  4698  ontri2orexmidim  4699  fvtp1  5900  nq0m0r  7787  nq02m  7796  gt0srpr  8079  map2psrprg  8136  pitoregt0  8180  axcnre  8212  addgt0  8739  addgegt0  8740  addgtge0  8741  addge0  8742  addgt0i  8779  addge0i  8780  addgegt0i  8781  add20i  8783  mulge0i  8911  recextlem1  8942  recap0  8976  recdivap  9009  recgt1  9188  prodgt0i  9199  prodge0i  9200  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  mulexpzap  10965  expaddzap  10969  m1expeven  10972  iexpcyc  11030  amgm2  11828  ege2le3  12382  sqnprm  12858  lmres  15239  2logb9irrap  15968