Theorem mpanl12 440

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reuun1  3515  ordtri2orexmid  4670  opthreg  4703  ordtri2or2exmid  4718  ontri2orexmidim  4719  fvtp1  5926  nq0m0r  7823  nq02m  7832  gt0srpr  8115  map2psrprg  8172  pitoregt0  8216  axcnre  8248  addgt0  8777  addgegt0  8778  addgtge0  8779  addge0  8780  addgt0i  8817  addge0i  8818  addgegt0i  8819  add20i  8821  mulge0i  8950  recextlem1  8981  recap0  9017  recdivap  9050  recgt1  9229  prodgt0i  9240  prodge0i  9241  iccshftri  10407  iccshftli  10409  iccdili  10411  icccntri  10413  mulexpzap  11029  expaddzap  11033  m1expeven  11036  iexpcyc  11094  amgm2  11899  ege2le3  12454  sqnprm  12931  prmlem1  13242  prmlem2  13254  lmres  15398  2logb9irrap  16132