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
mpanr1.2

Assertion

Ref	Expression
mpanr1

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2
2		mpanr1.2	. . 3
3	2	anassrs 648	. 2
4	1, 3	mpanl2 681	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  mpanr12  685  oacl  7204  omcl  7205  oaordi  7214  oawordri  7218  oaass  7229  oarec  7230  omordi  7234  omwordri  7240  odi  7247  omass  7248  oeoelem  7266  fimax2g  7786  noinfepOLD  8098  axcnre  9562  divdiv23zi  10322  recp1lt1  10468  divgt0i  10479  divge0i  10480  ltreci  10481  lereci  10482  lt2msqi  10483  le2msqi  10484  msq11i  10485  ltdiv23i  10495  ltdivp1i  10497  zmin  11207  ge0gtmnf  11402  hashprg  12460  sqrt11i  13217  sqrtmuli  13218  sqrtmsq2i  13220  sqrtlei  13221  sqrtlti  13222  cos01gt0  13926  0wlk  24547  0trl  24548  0pth  24572  0spth  24573  0crct  24626  0cycl  24627  0clwlk  24765  vc2  25448  vc0  25462  vcm  25464  vcnegneg  25467  nvnncan  25558  nvpi  25569  nvge0  25577  ipval3  25619  ipidsq  25623  sspmval  25646  opsqrlem1  27059  opsqrlem6  27064  hstle  27149  hstrbi  27185  atordi  27303

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