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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reuun1  3515  ordtri2orexmid  4672  opthreg  4705  ordtri2or2exmid  4720  ontri2orexmidim  4721  fvtp1  5929  nq0m0r  7829  nq02m  7838  gt0srpr  8121  map2psrprg  8178  pitoregt0  8222  axcnre  8254  addgt0  8783  addgegt0  8784  addgtge0  8785  addge0  8786  addgt0i  8823  addge0i  8824  addgegt0i  8825  add20i  8827  mulge0i  8956  recextlem1  8987  recap0  9023  recdivap  9056  recgt1  9235  prodgt0i  9246  prodge0i  9247  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  mulexpzap  11037  expaddzap  11041  m1expeven  11044  iexpcyc  11102  amgm2  11907  ege2le3  12463  sqnprm  12940  prmlem1  13251  prmlem2  13263  lmres  15474  2logb9irrap  16213  bposlem7  16317