Theorem mpanr1 683

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanr1.1	|- ps
mpanr1.2	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
mpanr1	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 |- ps
2		mpanr1.2	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	anassrs 648	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 681	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  mpanr12  685  oacl  6975  omcl  6976  oaordi  6985  oawordri  6989  oaass  7000  oarec  7001  omordi  7005  omwordri  7011  odi  7018  omass  7019  oeoelem  7037  fimax2g  7558  noinfepOLD  7866  axcnre  9331  divdiv23zi  10084  recp1lt1  10230  divgt0i  10241  divge0i  10242  ltreci  10243  lereci  10244  lt2msqi  10245  le2msqi  10246  msq11i  10247  ltdiv23i  10257  ltdivp1i  10259  zmin  10949  ge0gtmnf  11144  hashprg  12155  sqr11i  12872  sqrmuli  12873  sqrmsq2i  12875  sqrlei  12876  sqrlti  12877  cos01gt0  13475  0wlk  23444  0trl  23445  0pth  23469  0spth  23470  0crct  23512  0cycl  23513  vc2  23933  vc0  23947  vcm  23949  vcnegneg  23952  nvnncan  24043  nvpi  24054  nvge0  24062  ipval3  24104  ipidsq  24108  sspmval  24131  opsqrlem1  25544  opsqrlem6  25549  hstle  25634  hstrbi  25670  atordi  25788  0clwlk  30428