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  7824  nq02m  7833  gt0srpr  8116  map2psrprg  8173  pitoregt0  8217  axcnre  8249  addgt0  8778  addgegt0  8779  addgtge0  8780  addge0  8781  addgt0i  8818  addge0i  8819  addgegt0i  8820  add20i  8822  mulge0i  8951  recextlem1  8982  recap0  9018  recdivap  9051  recgt1  9230  prodgt0i  9241  prodge0i  9242  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  mulexpzap  11031  expaddzap  11035  m1expeven  11038  iexpcyc  11096  amgm2  11901  ege2le3  12457  sqnprm  12934  prmlem1  13245  prmlem2  13257  lmres  15440  2logb9irrap  16174  bposlem7  16278