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  3262  ordtri2orexmid  4294  opthreg  4327  ordtri2or2exmid  4342  fvtp1  5424  nq0m0r  6760  nq02m  6769  gt0srpr  7039  pitoregt0  7131  axcnre  7161  addgt0  7671  addgegt0  7672  addgtge0  7673  addge0  7674  addgt0i  7708  addge0i  7709  addgegt0i  7710  add20i  7712  mulge0i  7839  recextlem1  7860  recap0  7892  recdivap  7925  recgt1  8094  prodgt0i  8105  prodge0i  8106  iccshftri  9145  iccshftli  9147  iccdili  9149  icccntri  9151  mulexpzap  9665  expaddzap  9669  m1expeven  9672  iexpcyc  9728  amgm2  10205  sqnprm  10724