Theorem mpanl12 433

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  reuun1  3404  ordtri2orexmid  4500  opthreg  4533  ordtri2or2exmid  4548  ontri2orexmidim  4549  fvtp1  5696  nq0m0r  7397  nq02m  7406  gt0srpr  7689  map2psrprg  7746  pitoregt0  7790  axcnre  7822  addgt0  8346  addgegt0  8347  addgtge0  8348  addge0  8349  addgt0i  8386  addge0i  8387  addgegt0i  8388  add20i  8390  mulge0i  8518  recextlem1  8548  recap0  8581  recdivap  8614  recgt1  8792  prodgt0i  8803  prodge0i  8804  iccshftri  9931  iccshftli  9933  iccdili  9935  icccntri  9937  mulexpzap  10495  expaddzap  10499  m1expeven  10502  iexpcyc  10559  amgm2  11060  ege2le3  11612  sqnprm  12068  lmres  12898  2logb9irrap  13545