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  4615  opthreg  4648  ordtri2or2exmid  4663  ontri2orexmidim  4664  fvtp1  5854  nq0m0r  7654  nq02m  7663  gt0srpr  7946  map2psrprg  8003  pitoregt0  8047  axcnre  8079  addgt0  8606  addgegt0  8607  addgtge0  8608  addge0  8609  addgt0i  8646  addge0i  8647  addgegt0i  8648  add20i  8650  mulge0i  8778  recextlem1  8809  recap0  8843  recdivap  8876  recgt1  9055  prodgt0i  9066  prodge0i  9067  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  mulexpzap  10813  expaddzap  10817  m1expeven  10820  iexpcyc  10878  amgm2  11644  ege2le3  12197  sqnprm  12673  lmres  14937  2logb9irrap  15666