Theorem mpanr1 681

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 646	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 679	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  mpanr12  683  oacl  7125  omcl  7126  oaordi  7135  oawordri  7139  oaass  7150  oarec  7151  omordi  7155  omwordri  7161  odi  7168  omass  7169  oeoelem  7187  fimax2g  7703  axcnre  9474  divdiv23zi  10236  recp1lt1  10381  divgt0i  10392  divge0i  10393  ltreci  10394  lereci  10395  lt2msqi  10396  le2msqi  10397  msq11i  10398  ltdiv23i  10408  ltdivp1i  10410  zmin  11119  ge0gtmnf  11316  hashprg  12387  sqrt11i  13242  sqrtmuli  13243  sqrtmsq2i  13245  sqrtlei  13246  sqrtlti  13247  cos01gt0  13951  0wlk  24693  0trl  24694  0pth  24718  0spth  24719  0crct  24772  0cycl  24773  0clwlk  24911  vc2  25590  vc0  25604  vcm  25606  vcnegneg  25609  nvnncan  25700  nvpi  25711  nvge0  25719  ipval3  25761  ipidsq  25765  sspmval  25788  opsqrlem1  27200  opsqrlem6  27205  hstle  27290  hstrbi  27326  atordi  27444