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  3486  ordtri2orexmid  4614  opthreg  4647  ordtri2or2exmid  4662  ontri2orexmidim  4663  fvtp1  5849  nq0m0r  7639  nq02m  7648  gt0srpr  7931  map2psrprg  7988  pitoregt0  8032  axcnre  8064  addgt0  8591  addgegt0  8592  addgtge0  8593  addge0  8594  addgt0i  8631  addge0i  8632  addgegt0i  8633  add20i  8635  mulge0i  8763  recextlem1  8794  recap0  8828  recdivap  8861  recgt1  9040  prodgt0i  9051  prodge0i  9052  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  mulexpzap  10796  expaddzap  10800  m1expeven  10803  iexpcyc  10861  amgm2  11624  ege2le3  12177  sqnprm  12653  lmres  14916  2logb9irrap  15645