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  7183  omcl  7184  oaordi  7193  oawordri  7197  oaass  7208  oarec  7209  omordi  7213  omwordri  7219  odi  7226  omass  7227  oeoelem  7245  fimax2g  7764  noinfepOLD  8075  axcnre  9539  divdiv23zi  10298  recp1lt1  10444  divgt0i  10455  divge0i  10456  ltreci  10457  lereci  10458  lt2msqi  10459  le2msqi  10460  msq11i  10461  ltdiv23i  10471  ltdivp1i  10473  zmin  11182  ge0gtmnf  11377  hashprg  12434  sqrt11i  13191  sqrtmuli  13192  sqrtmsq2i  13194  sqrtlei  13195  sqrtlti  13196  cos01gt0  13798  0wlk  24412  0trl  24413  0pth  24437  0spth  24438  0crct  24491  0cycl  24492  0clwlk  24630  vc2  25313  vc0  25327  vcm  25329  vcnegneg  25332  nvnncan  25423  nvpi  25434  nvge0  25442  ipval3  25484  ipidsq  25488  sspmval  25511  opsqrlem1  26924  opsqrlem6  26929  hstle  27014  hstrbi  27050  atordi  27168