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  3487  ordtri2orexmid  4619  opthreg  4652  ordtri2or2exmid  4667  ontri2orexmidim  4668  fvtp1  5860  nq0m0r  7666  nq02m  7675  gt0srpr  7958  map2psrprg  8015  pitoregt0  8059  axcnre  8091  addgt0  8618  addgegt0  8619  addgtge0  8620  addge0  8621  addgt0i  8658  addge0i  8659  addgegt0i  8660  add20i  8662  mulge0i  8790  recextlem1  8821  recap0  8855  recdivap  8888  recgt1  9067  prodgt0i  9078  prodge0i  9079  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  mulexpzap  10831  expaddzap  10835  m1expeven  10838  iexpcyc  10896  amgm2  11669  ege2le3  12222  sqnprm  12698  lmres  14962  2logb9irrap  15691