Theorem mpanl12 436

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 434	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  reuun1  3419  ordtri2orexmid  4524  opthreg  4557  ordtri2or2exmid  4572  ontri2orexmidim  4573  fvtp1  5729  nq0m0r  7457  nq02m  7466  gt0srpr  7749  map2psrprg  7806  pitoregt0  7850  axcnre  7882  addgt0  8407  addgegt0  8408  addgtge0  8409  addge0  8410  addgt0i  8447  addge0i  8448  addgegt0i  8449  add20i  8451  mulge0i  8579  recextlem1  8610  recap0  8644  recdivap  8677  recgt1  8856  prodgt0i  8867  prodge0i  8868  iccshftri  9997  iccshftli  9999  iccdili  10001  icccntri  10003  mulexpzap  10562  expaddzap  10566  m1expeven  10569  iexpcyc  10627  amgm2  11129  ege2le3  11681  sqnprm  12138  lmres  13833  2logb9irrap  14480