Theorem mpanr1 719

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  mpanr12  721  oacl  7615  omcl  7616  oaordi  7626  oawordri  7630  oaass  7641  oarec  7642  omordi  7646  omwordri  7652  odi  7659  omass  7660  oeoelem  7678  fimax2g  8206  fimin2g  8403  axcnre  9985  divdiv23zi  10778  recp1lt1  10921  divgt0i  10932  divge0i  10933  ltreci  10934  lereci  10935  lt2msqi  10936  le2msqi  10937  msq11i  10938  ltdiv23i  10948  ltdivp1i  10950  zmin  11784  ge0gtmnf  12003  hashprg  13182  hashprgOLD  13183  sqrt11i  14124  sqrtmuli  14125  sqrtmsq2i  14127  sqrtlei  14128  sqrtlti  14129  cos01gt0  14921  vc2OLD  27423  vc0  27429  vcm  27431  nvpi  27522  nvge0  27528  ipval3  27564  ipidsq  27565  sspmval  27588  opsqrlem1  28999  opsqrlem6  29004  hstle  29089  hstrbi  29125  atordi  29243  poimirlem6  33415  poimirlem7  33416  poimirlem16  33425  poimirlem19  33428  poimirlem20  33429