Theorem mpanr1 694

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  mpanr12  696  oacl  7262  omcl  7263  oaordi  7272  oawordri  7276  oaass  7287  oarec  7288  omordi  7292  omwordri  7298  odi  7305  omass  7306  oeoelem  7324  fimax2g  7842  fimin2g  8038  axcnre  9613  divdiv23zi  10387  recp1lt1  10531  divgt0i  10542  divge0i  10543  ltreci  10544  lereci  10545  lt2msqi  10546  le2msqi  10547  msq11i  10548  ltdiv23i  10558  ltdivp1i  10560  zmin  11288  ge0gtmnf  11495  hashprg  12603  sqrt11i  13495  sqrtmuli  13496  sqrtmsq2i  13498  sqrtlei  13499  sqrtlti  13500  cos01gt0  14293  0wlk  25323  0trl  25324  0pth  25348  0spth  25349  0crct  25402  0cycl  25403  0clwlk  25541  vc2  26222  vc0  26236  vcm  26238  vcnegneg  26241  nvnncan  26332  nvpi  26343  nvge0  26351  ipval3  26393  ipidsq  26397  sspmval  26420  opsqrlem1  27841  opsqrlem6  27846  hstle  27931  hstrbi  27967  atordi  28085  poimirlem6  31990  poimirlem7  31991  poimirlem16  32000  poimirlem19  32003  poimirlem20  32004