Theorem mpanl12 427

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  reuun1  3281  ordtri2orexmid  4339  opthreg  4372  ordtri2or2exmid  4387  fvtp1  5508  nq0m0r  7015  nq02m  7024  gt0srpr  7294  pitoregt0  7386  axcnre  7416  addgt0  7926  addgegt0  7927  addgtge0  7928  addge0  7929  addgt0i  7966  addge0i  7967  addgegt0i  7968  add20i  7970  mulge0i  8097  recextlem1  8120  recap0  8152  recdivap  8185  recgt1  8358  prodgt0i  8369  prodge0i  8370  iccshftri  9412  iccshftli  9414  iccdili  9416  icccntri  9418  mulexpzap  9995  expaddzap  9999  m1expeven  10002  iexpcyc  10059  amgm2  10551  ege2le3  10961  sqnprm  11395