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  3441  ordtri2orexmid  4555  opthreg  4588  ordtri2or2exmid  4603  ontri2orexmidim  4604  fvtp1  5769  nq0m0r  7516  nq02m  7525  gt0srpr  7808  map2psrprg  7865  pitoregt0  7909  axcnre  7941  addgt0  8467  addgegt0  8468  addgtge0  8469  addge0  8470  addgt0i  8507  addge0i  8508  addgegt0i  8509  add20i  8511  mulge0i  8639  recextlem1  8670  recap0  8704  recdivap  8737  recgt1  8916  prodgt0i  8927  prodge0i  8928  iccshftri  10061  iccshftli  10063  iccdili  10065  icccntri  10067  mulexpzap  10650  expaddzap  10654  m1expeven  10657  iexpcyc  10715  amgm2  11262  ege2le3  11814  sqnprm  12274  lmres  14416  2logb9irrap  15109