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  3491  ordtri2orexmid  4627  opthreg  4660  ordtri2or2exmid  4675  ontri2orexmidim  4676  fvtp1  5873  nq0m0r  7719  nq02m  7728  gt0srpr  8011  map2psrprg  8068  pitoregt0  8112  axcnre  8144  addgt0  8670  addgegt0  8671  addgtge0  8672  addge0  8673  addgt0i  8710  addge0i  8711  addgegt0i  8712  add20i  8714  mulge0i  8842  recextlem1  8873  recap0  8907  recdivap  8940  recgt1  9119  prodgt0i  9130  prodge0i  9131  iccshftri  10274  iccshftli  10276  iccdili  10278  icccntri  10280  mulexpzap  10887  expaddzap  10891  m1expeven  10894  iexpcyc  10952  amgm2  11741  ege2le3  12295  sqnprm  12771  lmres  15042  2logb9irrap  15771