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  3489  ordtri2orexmid  4621  opthreg  4654  ordtri2or2exmid  4669  ontri2orexmidim  4670  fvtp1  5864  nq0m0r  7675  nq02m  7684  gt0srpr  7967  map2psrprg  8024  pitoregt0  8068  axcnre  8100  addgt0  8627  addgegt0  8628  addgtge0  8629  addge0  8630  addgt0i  8667  addge0i  8668  addgegt0i  8669  add20i  8671  mulge0i  8799  recextlem1  8830  recap0  8864  recdivap  8897  recgt1  9076  prodgt0i  9087  prodge0i  9088  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  mulexpzap  10840  expaddzap  10844  m1expeven  10847  iexpcyc  10905  amgm2  11678  ege2le3  12231  sqnprm  12707  lmres  14971  2logb9irrap  15700