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  7175  omcl  7176  oaordi  7185  oawordri  7189  oaass  7200  oarec  7201  omordi  7205  omwordri  7211  odi  7218  omass  7219  oeoelem  7237  fimax2g  7755  noinfepOLD  8066  axcnre  9530  divdiv23zi  10286  recp1lt1  10432  divgt0i  10443  divge0i  10444  ltreci  10445  lereci  10446  lt2msqi  10447  le2msqi  10448  msq11i  10449  ltdiv23i  10459  ltdivp1i  10461  zmin  11167  ge0gtmnf  11362  hashprg  12415  sqr11i  13166  sqrmuli  13167  sqrmsq2i  13169  sqrlei  13170  sqrlti  13171  cos01gt0  13776  0wlk  24209  0trl  24210  0pth  24234  0spth  24235  0crct  24288  0cycl  24289  0clwlk  24427  vc2  25110  vc0  25124  vcm  25126  vcnegneg  25129  nvnncan  25220  nvpi  25231  nvge0  25239  ipval3  25281  ipidsq  25285  sspmval  25308  opsqrlem1  26721  opsqrlem6  26726  hstle  26811  hstrbi  26847  atordi  26965