Theorem mpanl12 433

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 431	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 421	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  reuun1  3363  ordtri2orexmid  4446  opthreg  4479  ordtri2or2exmid  4494  fvtp1  5639  nq0m0r  7288  nq02m  7297  gt0srpr  7580  map2psrprg  7637  pitoregt0  7681  axcnre  7713  addgt0  8234  addgegt0  8235  addgtge0  8236  addge0  8237  addgt0i  8274  addge0i  8275  addgegt0i  8276  add20i  8278  mulge0i  8406  recextlem1  8436  recap0  8469  recdivap  8502  recgt1  8679  prodgt0i  8690  prodge0i  8691  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  mulexpzap  10364  expaddzap  10368  m1expeven  10371  iexpcyc  10428  amgm2  10922  ege2le3  11414  sqnprm  11852  lmres  12456  2logb9irrap  13102