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  3442  ordtri2orexmid  4556  opthreg  4589  ordtri2or2exmid  4604  ontri2orexmidim  4605  fvtp1  5770  nq0m0r  7518  nq02m  7527  gt0srpr  7810  map2psrprg  7867  pitoregt0  7911  axcnre  7943  addgt0  8469  addgegt0  8470  addgtge0  8471  addge0  8472  addgt0i  8509  addge0i  8510  addgegt0i  8511  add20i  8513  mulge0i  8641  recextlem1  8672  recap0  8706  recdivap  8739  recgt1  8918  prodgt0i  8929  prodge0i  8930  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  mulexpzap  10653  expaddzap  10657  m1expeven  10660  iexpcyc  10718  amgm2  11265  ege2le3  11817  sqnprm  12277  lmres  14427  2logb9irrap  15150