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  10413  iccshftli  10415  iccdili  10417  icccntri  10419  mulexpzap  11036  expaddzap  11040  m1expeven  11043  iexpcyc  11101  amgm2  11906  ege2le3  12462  sqnprm  12939  prmlem1  13250  prmlem2  13262  lmres  15491  2logb9irrap  16230  bposlem7  16334