Theorem mp3anr1 1321

Description: An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)

Hypotheses

Ref	Expression
mp3anr1.1
mp3anr1.2

Assertion

Ref	Expression
mp3anr1

Proof of Theorem mp3anr1

Step	Hyp	Ref	Expression
1		mp3anr1.1	. . 3
2		mp3anr1.2	. . . 4
3	2	ancoms 453	. . 3
4	1, 3	mp3anl1 1318	. 2
5	4	ancoms 453	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  vc2  25448  vcsubdir  25449  vc0  25462  vcm  25464  vcnegneg  25467  vcnegsubdi2  25468  vcsub4  25469  nvaddsub4  25556  nvnncan  25558  nvpi  25569  nvge0  25577  ipval3  25619  ipidsq  25623  lnoadd  25673  lnosub  25674  dipsubdir  25763

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  df-3an 975