Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  equncomiVD Structured version   Unicode version

Theorem equncomiVD 36909
Description: Inference form of equncom 3617. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. equncomi 3618 is equncomiVD 36909 without virtual deductions and was automatically derived from equncomiVD 36909.
h1::  |-  A  =  ( B  u.  C )
qed:1:  |-  A  =  ( C  u.  B )
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
equncomiVD.1  |-  A  =  ( B  u.  C
)
Assertion
Ref Expression
equncomiVD  |-  A  =  ( C  u.  B
)

Proof of Theorem equncomiVD
StepHypRef Expression
1 equncomiVD.1 . 2  |-  A  =  ( B  u.  C
)
2 equncom 3617 . . 3  |-  ( A  =  ( B  u.  C )  <->  A  =  ( C  u.  B
) )
32biimpi 197 . 2  |-  ( A  =  ( B  u.  C )  ->  A  =  ( C  u.  B ) )
41, 3e0a 36802 1  |-  A  =  ( C  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator