Theorem mpanl12 440

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 438	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 428	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  3515  ordtri2orexmid  4665  opthreg  4698  ordtri2or2exmid  4713  ontri2orexmidim  4714  fvtp1  5917  nq0m0r  7813  nq02m  7822  gt0srpr  8105  map2psrprg  8162  pitoregt0  8206  axcnre  8238  addgt0  8766  addgegt0  8767  addgtge0  8768  addge0  8769  addgt0i  8806  addge0i  8807  addgegt0i  8808  add20i  8810  mulge0i  8938  recextlem1  8969  recap0  9005  recdivap  9038  recgt1  9217  prodgt0i  9228  prodge0i  9229  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  mulexpzap  10994  expaddzap  10998  m1expeven  11001  iexpcyc  11059  amgm2  11862  ege2le3  12416  sqnprm  12892  lmres  15272  2logb9irrap  16002