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  4670  opthreg  4703  ordtri2or2exmid  4718  ontri2orexmidim  4719  fvtp1  5926  nq0m0r  7823  nq02m  7832  gt0srpr  8115  map2psrprg  8172  pitoregt0  8216  axcnre  8248  addgt0  8776  addgegt0  8777  addgtge0  8778  addge0  8779  addgt0i  8816  addge0i  8817  addgegt0i  8818  add20i  8820  mulge0i  8948  recextlem1  8979  recap0  9015  recdivap  9048  recgt1  9227  prodgt0i  9238  prodge0i  9239  iccshftri  10397  iccshftli  10399  iccdili  10401  icccntri  10403  mulexpzap  11016  expaddzap  11020  m1expeven  11023  iexpcyc  11081  amgm2  11884  ege2le3  12438  sqnprm  12914  lmres  15349  2logb9irrap  16079