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  3446  ordtri2orexmid  4560  opthreg  4593  ordtri2or2exmid  4608  ontri2orexmidim  4609  fvtp1  5776  nq0m0r  7540  nq02m  7549  gt0srpr  7832  map2psrprg  7889  pitoregt0  7933  axcnre  7965  addgt0  8492  addgegt0  8493  addgtge0  8494  addge0  8495  addgt0i  8532  addge0i  8533  addgegt0i  8534  add20i  8536  mulge0i  8664  recextlem1  8695  recap0  8729  recdivap  8762  recgt1  8941  prodgt0i  8952  prodge0i  8953  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  mulexpzap  10688  expaddzap  10692  m1expeven  10695  iexpcyc  10753  amgm2  11300  ege2le3  11853  sqnprm  12329  lmres  14568  2logb9irrap  15297