P. 367 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

uunT1 36601

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accomodate a possible future version of df-tru 1408. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ph ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT1p1 36602

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ T. ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT21 36603

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun121 36604

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun121p1 36605

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun132 36606

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun132p1 36607

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ps /\ ch ) /\ ph ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

anabss7p1 36608

A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 822. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ps /\ ph ) /\ ph ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )

Theorem

un10 36609

A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

|- (. (. ph ,. T. ). ->. ps ).   =>    |- (. ph ->. ps ).

Theorem

un01 36610

A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

|- (. (. T. ,. ph ). ->. ps ).   =>    |- (. ph ->. ps ).

Theorem

un2122 36611

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) /\ ps /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun2131 36612

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun2131p1 36613

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ch ) /\ ( ph /\ ps ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uunTT1 36614

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ T. /\ ph ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunTT1p1 36615

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ph /\ T. ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunTT1p2 36616

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ T. /\ T. ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT11 36617

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ph /\ ph ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT11p1 36618

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ T. /\ ph ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT11p2 36619

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ph /\ T. ) -> ps )   =>    |- ( ph -> ps )

Theorem

uunT12 36620

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uunT12p1 36621

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( T. /\ ps /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uunT12p2 36622

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ T. /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uunT12p3 36623

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ps /\ T. /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uunT12p4 36624

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ps /\ T. ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uunT12p5 36625

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ps /\ ph /\ T. ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun111 36626

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ph /\ ph ) -> ps )   =>    |- ( ph -> ps )

Theorem

3anidm12p1 36627

A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1287 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ps /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

3anidm12p2 36628

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ps /\ ph /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )

Theorem

uun123 36629

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ch /\ ps ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun123p1 36630

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ps /\ ph /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun123p2 36631

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ch /\ ph /\ ps ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun123p3 36632

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ps /\ ch /\ ph ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun123p4 36633

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ch /\ ps /\ ph ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )

Theorem

uun2221 36634

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ph /\ ( ps /\ ph ) ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )

Theorem

uun2221p1 36635

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ( ps /\ ph ) /\ ph ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )

Theorem

uun2221p2 36636

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ps /\ ph ) /\ ph /\ ph ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )

Theorem

3impdirp1 36637

A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1286. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ch /\ ps ) /\ ( ph /\ ps ) ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )

Theorem

3impcombi 36638

A 1-hypothesis propositional calculus deduction (Contributed by Alan Sare, 25-Sep-2017.)

|- ( ( ph /\ ps /\ ph ) -> ( ch <-> th ) )   =>    |- ( ( ps /\ ph /\ ch ) -> th )

Theorem

3imp231 36639

Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)

|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ch /\ ph ) -> th )

21.29.7  Theorems proved using Virtual Deduction

Theorem

trsspwALT 36640

Virtual deduction proof of the left-to-right implication of dftr4 4494. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4494 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> A C_ ~P A )

Theorem

trsspwALT2 36641

Virtual deduction proof of trsspwALT 36640. This proof is the same as the proof of trsspwALT 36640 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> A C_ ~P A )

Theorem

trsspwALT3 36642

Short predicate calculus proof of the left-to-right implication of dftr4 4494. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 36641, which is the virtual deduction proof trsspwALT 36640 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> A C_ ~P A )

Theorem

sspwtr 36643

Virtual deduction proof of the right-to-left implication of dftr4 4494. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 36643 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A C_ ~P A -> Tr A )

Theorem

sspwtrALT 36644

Virtual deduction proof of sspwtr 36643. This proof is the same as the proof of sspwtr 36643 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A C_ ~P A -> Tr A )

Theorem

csbabgOLD 36645*

Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) Obsolete as of 19-Aug-2018. Use csbab 3802 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph } )

Theorem

csbunigOLD 36646

Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 22-Aug-2018. Use csbuni 4219 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )

Theorem

csbfv12gALTOLD 36647

Move class substitution in and out of a function value. The proof is derived from the virtual deduction proof csbfv12gALTVD 36730. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5884 instead. (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )

Theorem

csbxpgOLD 36648

Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5285 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. D -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )

Theorem

csbingOLD 36649

Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) Obsolete as of 18-Aug-2018. Use csbin 3804 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )

Theorem

csbresgOLD 36650

Distribute proper substitution through the restriction of a class. csbresgOLD 36650 is derived from the virtual deduction proof csbresgVD 36726. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbres 5097 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )

Theorem

csbrngOLD 36651

Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5285 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )

Theorem

csbima12gALTOLD 36652

Move class substitution in and out of the image of a function. The proof is derived from the virtual deduction proof csbima12gALTVD 36728. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5884 instead. (Proof modification is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )

Theorem

sspwtrALT2 36653

Short predicate calculus proof of the right-to-left implication of dftr4 4494. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 36644, which is the virtual deduction proof sspwtr 36643 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A C_ ~P A -> Tr A )

Theorem

pwtrVD 36654

Virtual deduction proof of pwtr 4644; see pwtrrVD 36655 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr ~P A )

Theorem

pwtrrVD 36655

Virtual deduction proof of pwtr 4644; see pwtrVD 36654 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A e. _V   =>    |- ( Tr ~P A -> Tr A )

Theorem

suctrALT 36656

The successor of a transitive class is transitive. The proof of http://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 36656 using completeusersproof, which is verified by the Metamath program. The proof of http://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 5493 for the original proof. (Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

snssiALTVD 36657

Virtual deduction proof of snssiALT 36658. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> { A } C_ B )

Theorem

snssiALT 36658

If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4116. This theorem was automatically generated from snssiALTVD 36657 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> { A } C_ B )

Theorem

snsslVD 36659

Virtual deduction proof of snssl 36660. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A e. _V   =>    |- ( { A } C_ B -> A e. B )

Theorem

snssl 36660

If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 4096. The proof of this theorem was automatically generated from snsslVD 36659 using a tools command file, translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A e. _V   =>    |- ( { A } C_ B -> A e. B )

Theorem

snelpwrVD 36661

Virtual deduction proof of snelpwi 4636. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> { A } e. ~P B )

Theorem

unipwrVD 36662

Virtual deduction proof of unipwr 36663. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A C_ U. ~P A

Theorem

unipwr 36663

A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4641. The proof of this theorem was automatically generated from unipwrVD 36662 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A C_ U. ~P A

Theorem

sstrALT2VD 36664

Virtual deduction proof of sstrALT2 36665. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A C_ B /\ B C_ C ) -> A C_ C )

Theorem

sstrALT2 36665

Virtual deduction proof of sstr 3450, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 36664 using the command file translate_without_overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A C_ B /\ B C_ C ) -> A C_ C )

Theorem

suctrALT2VD 36666

Virtual deduction proof of suctrALT2 36667. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

suctrALT2 36667

Virtual deduction proof of suctr 5493. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 36666 using the tools command file translate_without_overwriting_minimize_excluding_duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

elex2VD 36668*

Virtual deduction proof of elex2 3071. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> E. x x e. B )

Theorem

elex22VD 36669*

Virtual deduction proof of elex22 3072. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )

Theorem

eqsbc3rVD 36670*

Virtual deduction proof of eqsbc3r 3334. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> ( [. A / x ]. C = x <-> C = A ) )

Theorem

zfregs2VD 36671*

Virtual deduction proof of zfregs2 8196. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )

Theorem

tpid3gVD 36672

Virtual deduction proof of tpid3g 4087. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> A e. { C , D , A } )

Theorem

en3lplem1VD 36673*

Virtual deduction proof of en3lplem1 8064. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) )

Theorem

en3lplem2VD 36674*

Virtual deduction proof of en3lplem2 8065. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )

Theorem

en3lpVD 36675

Virtual deduction proof of en3lp 8066. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- -. ( A e. B /\ B e. C /\ C e. A )

21.29.8  Theorems proved using Virtual Deduction with mmj2 assistance

Theorem

simplbi2VD 36676

Virtual deduction proof of simplbi2 623. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ( ph <-> ( ps /\ ch ) )
3:1,?: e0a 36593	|- ( ( ps /\ ch ) -> ph )
qed:3,?: e0a 36593	|- ( ps -> ( ch -> ph ) )

The proof of simplbi2 623 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch -> ph ) )

Theorem

3ornot23VD 36677

Virtual deduction proof of 3ornot23 36295. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::

|- (. ( -. ph /\ -. ps ) ->. ( -. ph /\ -. ps ) ).
2::	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ph \/ ps ) ).
3:1,?: e1a 36437	|- (. ( -. ph /\ -. ps ) ->. -. ph ).
4:1,?: e1a 36437	|- (. ( -. ph /\ -. ps ) ->. -. ps ).
5:3,4,?: e11 36498	|- (. ( -. ph /\ -. ps ) ->. -. ( ph \/ ps ) ).
6:2,?: e2 36441	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ( ph \/ ps ) ) ).
7:5,6,?: e12 36545	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ch ).
8:7:	|- (. ( -. ph /\ -. ps ) ->. ( ( ch \/ ph \/ ps ) -> ch ) ).
qed:8:	|- ( ( -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) )

Theorem

orbi1rVD 36678

Virtual deduction proof of orbi1r 36296. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph <-> ps ) ->. ( ph <-> ps ) ).
2::	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ch \/ ph ) ).
3:2,?: e2 36441	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ph \/ ch ) ).
4:1,3,?: e12 36545	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ps \/ ch ) ).
5:4,?: e2 36441	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ch \/ ps ) ).
6:5:	|- (. ( ph <-> ps ) ->. ( ( ch \/ ph ) -> ( ch \/ ps ) ) ).
7::	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ps ) ).
8:7,?: e2 36441	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ps \/ ch ) ).
9:1,8,?: e12 36545	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ph \/ ch ) ).
10:9,?: e2 36441	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ph ) ).
11:10:	|- (. ( ph <-> ps ) ->. ( ( ch \/ ps ) -> ( ch \/ ph ) ) ).
12:6,11,?: e11 36498	|- (. ( ph <-> ps ) ->. ( ( ch \/ ph ) <-> ( ch \/ ps ) ) ).
qed:12:	|- ( ( ph <-> ps ) -> ( ( ch \/ ph ) <-> ( ch \/ ps ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph <-> ps ) -> ( ( ch \/ ph ) <-> ( ch \/ ps ) ) )

Theorem

bitr3VD 36679

Virtual deduction proof of bitr3 36297. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph <-> ps ) ->. ( ph <-> ps ) ).
2:1,?: e1a 36437	|- (. ( ph <-> ps ) ->. ( ps <-> ph ) ).
3::	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ph <-> ch ) ).
4:3,?: e2 36441	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ch <-> ph ) ).
5:2,4,?: e12 36545	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ps <-> ch ) ).
6:5:	|- (. ( ph <-> ps ) ->. ( ( ph <-> ch ) -> ( ps <-> ch ) ) ).
qed:6:	|- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) )

Theorem

3orbi123VD 36680

Virtual deduction proof of 3orbi123 36298. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ).
2:1,?: e1a 36437	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ph <-> ps ) ).
3:1,?: e1a 36437	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ch <-> th ) ).
4:1,?: e1a 36437	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ta <-> et ) ).
5:2,3,?: e11 36498	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch ) <-> ( ps \/ th ) ) ).
6:5,4,?: e11 36498	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
7:?:	|- ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) )
8:6,7,?: e10 36504	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
9:?:	|- ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) )
10:8,9,?: e10 36504	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) ).
qed:10:	|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )

Theorem

sbc3orgVD 36681

Virtual deduction proof of sbc3orgOLD 36323. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A e. B ->. A e. B ).
2:1,?: e1a 36437	|- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
3::	|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) )
32:3:	|- A. x ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) )
33:1,32,?: e10 36504	|- (. A e. B ->. [. A / x ]. ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) ) ).
4:1,33,?: e11 36498	|- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) ) ).
5:2,4,?: e11 36498	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
6:1,?: e1a 36437	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) ).
7:6,?: e1a 36437	|- (. A e. B ->. ( ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
8:5,7,?: e11 36498	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
9:?:	|- ( ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) )
10:8,9,?: e10 36504	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) ) ).
qed:10:	|- ( A e. B -> ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) ) )

Theorem

19.21a3con13vVD 36682*

Virtual deduction proof of alrim3con13v 36324. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
2::	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
3:2,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12 36545	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222 36446	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2 36441	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
11:10:in2	|- (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
qed:11:in1	|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Theorem

exbirVD 36683

Virtual deduction proof of exbir 36237. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( ch <-> th ) ) ).
2::	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ->. ( ph /\ ps ) ).
3::	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) , th ->. th ).
5:1,2,?: e12 36545	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( ch <-> th ) ).
6:3,5,?: e32 36579	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) , th ->. ch ).
7:6:	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( th -> ch ) ).
8:7:	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( th -> ch ) ) ).
9:8,?: e1a 36437	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ph -> ( ps -> ( th -> ch ) ) ) ).
qed:9:	|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

Theorem

exbiriVD 36684

Virtual deduction proof of exbiri 620. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ( ( ph /\ ps ) -> ( ch <-> th ) )
2::	|- (. ph ->. ph ).
3::	|- (. ph ,. ps ->. ps ).
4::	|- (. ph ,. ps ,. th ->. th ).
5:2,1,?: e10 36504	|- (. ph ->. ( ps -> ( ch <-> th ) ) ).
6:3,5,?: e21 36551	|- (. ph ,. ps ->. ( ch <-> th ) ).
7:4,6,?: e32 36579	|- (. ph ,. ps ,. th ->. ch ).
8:7:	|- (. ph ,. ps ->. ( th -> ch ) ).
9:8:	|- (. ph ->. ( ps -> ( th -> ch ) ) ).
qed:9:	|- ( ph -> ( ps -> ( th -> ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ph -> ( ps -> ( th -> ch ) ) )

Theorem

rspsbc2VD 36685*

Virtual deduction proof of rspsbc2 36325. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A e. B ->. A e. B ).
2::	|- (. A e. B ,. C e. D ->. C e. D ).
3::	|- (. A e. B ,. C e. D ,. A. x e. B A. y e. D ph ->. A. x e. B A. y e. D ph ).
4:1,3,?: e13 36569	|- (. A e. B ,. C e. D ,. A. x e. B A. y e. D ph ->. [. A / x ]. A. y e. D ph ).
5:1,4,?: e13 36569	|- (. A e. B ,. C e. D ,. A. x e. B A. y e. D ph ->. A. y e. D [. A / x ]. ph ).
6:2,5,?: e23 36576	|- (. A e. B ,. C e. D ,. A. x e. B A. y e. D ph ->. [. C / y ]. [. A / x ]. ph ).
7:6:	|- (. A e. B ,. C e. D ->. ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ).
8:7:	|- (. A e. B ->. ( C e. D -> ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ) ).
qed:8:	|- ( A e. B -> ( C e. D -> ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> ( C e. D -> ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ) )

Theorem

3impexpVD 36686

Virtual deduction proof of 3impexp 1219. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
2::	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
3:1,2,?: e10 36504	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
4:3,?: e1a 36437	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
5:4,?: e1a 36437	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
6:5:	|- ( ( ( ph /\ ps /\ ch ) -> th ) -> ( ph -> ( ps -> ( ch -> th ) ) ) )
7::	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
8:7,?: e1a 36437	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
9:8,?: e1a 36437	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
10:2,9,?: e01 36501	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
11:10:	|- ( ( ph -> ( ps -> ( ch -> th ) ) ) -> ( ( ph /\ ps /\ ch ) -> th ) )
qed:6,11,?: e00 36589	|- ( ( ( ph /\ ps /\ ch ) -> th ) <-> ( ph -> ( ps -> ( ch -> th ) ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps /\ ch ) -> th ) <-> ( ph -> ( ps -> ( ch -> th ) ) ) )

Theorem

3impexpbicomVD 36687

Virtual deduction proof of 3impexpbicom 36238. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ).
2::	|- ( ( th <-> ta ) <-> ( ta <-> th ) )
3:1,2,?: e10 36504	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
4:3,?: e1a 36437	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ).
5:4:	|- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )
6::	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ).
7:6,?: e1a 36437	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
8:7,2,?: e10 36504	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ).
9:8:	|- ( ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) -> ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) )
qed:5,9,?: e00 36589	|- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )

Theorem

3impexpbicomiVD 36688

Virtual deduction proof of 3impexpbicomi 36239. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )
qed:1,?: e0a 36593	|- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) )

Theorem

sbcel1gvOLD 36689*

Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 17-Aug-2018. Use sbcel1v 3336 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> ( [. A / x ]. x e. B <-> A e. B ) )

Theorem

sbcoreleleqVD 36690*

Virtual deduction proof of sbcoreleleq 36326. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A e. B ->. A e. B ).
2:1,?: e1a 36437	|- (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
3:1,?: e1a 36437	|- (. A e. B ->. ( [. A / y ]. y e. x <-> A e. x ) ).
4:1,?: e1a 36437	|- (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
5:2,3,4,?: e111 36484	|- (. A e. B ->. ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
6:1,?: e1a 36437	|- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
7:5,6: e11 36498	|- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ).
qed:7:	|- ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )

Theorem

hbra2VD 36691*

Virtual deduction proof of nfra2 2791. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- ( A. y e. B A. x e. A ph -> A. y A. y e. B A. x e. A ph )
2::	|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
3:1,2,?: e00 36589	|- ( A. x e. A A. y e. B ph -> A. y A. y e. B A. x e. A ph )
4:2:	|- A. y ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
5:4,?: e0a 36593	|- ( A. y A. x e. A A. y e. B ph <-> A. y A. y e. B A. x e. A ph )
qed:3,5,?: e00 36589	|- ( A. x e. A A. y e. B ph -> A. y A. x e. A A. y e. B ph )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A. x e. A A. y e. B ph -> A. y A. x e. A A. y e. B ph )

Theorem

tratrbVD 36692*

Virtual deduction proof of tratrb 36327. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ).
2:1,?: e1a 36437	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr A ).
3:1,?: e1a 36437	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
4:1,?: e1a 36437	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. B e. A ).
5::	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. y /\ y e. B ) ).
6:5,?: e2 36441	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. y ).
7:5,?: e2 36441	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. B ).
8:2,7,4,?: e121 36466	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. A ).
9:2,6,8,?: e122 36463	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. A ).
10::	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. B e. x ).
11:6,7,10,?: e223 36445	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. ( x e. y /\ y e. B /\ B e. x ) ).
12:11:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( B e. x -> ( x e. y /\ y e. B /\ B e. x ) ) ).
13::	|- -. ( x e. y /\ y e. B /\ B e. x )
14:12,13,?: e20 36548	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. B e. x ).
15::	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. x = B ).
16:7,15,?: e23 36576	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. y e. x ).
17:6,16,?: e23 36576	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. ( x e. y /\ y e. x ) ).
18:17:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x = B -> ( x e. y /\ y e. x ) ) ).
19::	|- -. ( x e. y /\ y e. x )
20:18,19,?: e20 36548	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. x = B ).
21:3,?: e1a 36437	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y e. A A. x e. A ( x e. y \/ y e. x \/ x = y ) ).
22:21,9,4,?: e121 36466	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. x / x ]. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
23:22,?: e2 36441	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
24:4,23,?: e12 36545	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. B \/ B e. x \/ x = B ) ).
25:14,20,24,?: e222 36446	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. B ).
26:25:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( ( x e. y /\ y e. B ) -> x e. B ) ).
27::	|- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. y A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
28:27,?: e0a 36593	|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. y ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
29:28,26:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
30::	|- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. x A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
31:30,?: e0a 36593	|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. x ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
32:31,29:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
33:32,?: e1a 36437	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr B ).
qed:33:	|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )

Theorem

al2imVD 36693

Virtual deduction proof of al2im 1656. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A. x ( ph -> ( ps -> ch ) ) ->. A. x ( ph -> ( ps -> ch ) ) ).
2:1,?: e1a 36437	|- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> A. x ( ps -> ch ) ) ).
3::	|- ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) )
4:2,3,?: e10 36504	|- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> ( A. x ps -> A. x ch ) ) ).
qed:4:	|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )

Theorem

syl5impVD 36694

Virtual deduction proof of syl5imp 36299. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph -> ( ps -> ch ) ) ->. ( ph -> ( ps -> ch ) ) ).
2:1,?: e1a 36437	|- (. ( ph -> ( ps -> ch ) ) ->. ( ps -> ( ph -> ch ) ) ).
3::	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ps ) ).
4:3,2,?: e21 36551	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ( ph -> ch ) ) ).
5:4,?: e2 36441	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( ph -> ( th -> ch ) ) ).
6:5:	|- (. ( ph -> ( ps -> ch ) ) ->. ( ( th -> ps ) -> ( ph -> ( th -> ch ) ) ) ).
qed:6:	|- ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ps ) -> ( ph -> ( th -> ch ) ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ps ) -> ( ph -> ( th -> ch ) ) ) )

Theorem

idiVD 36695

Virtual deduction proof of idiALT 36236. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ph
qed:1,?: e0a 36593	|- ph

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ph   =>    |- ph

Theorem

ancomstVD 36696

Closed form of ancoms 451. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
qed:1,?: e0a 36593	|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )

The proof of ancomst 450 is derived automatically from it. (Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )

Theorem

ssralv2VD 36697*

Quantification restricted to a subclass for two quantifiers. ssralv 3503 for two quantifiers. 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. ssralv2 36318 is ssralv2VD 36697 without virtual deductions and was automatically derived from ssralv2VD 36697.

1::	|- (. ( A C_ B /\ C C_ D ) ->. ( A C_ B /\ C C_ D ) ).
2::	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. A. x e. B A. y e. D ph ).
3:1:	|- (. ( A C_ B /\ C C_ D ) ->. A C_ B ).
4:3,2:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. A. x e. A A. y e. D ph ).
5:4:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. A. x ( x e. A -> A. y e. D ph ) ).
6:5:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. ( x e. A -> A. y e. D ph ) ).
7::	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph , x e. A ->. x e. A ).
8:7,6:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph , x e. A ->. A. y e. D ph ).
9:1:	|- (. ( A C_ B /\ C C_ D ) ->. C C_ D ).
10:9,8:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph , x e. A ->. A. y e. C ph ).
11:10:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. ( x e. A -> A. y e. C ph ) ).
12::	|- ( ( A C_ B /\ C C_ D ) -> A. x ( A C_ B /\ C C_ D ) )
13::	|- ( A. x e. B A. y e. D ph -> A. x A. x e. B A. y e. D ph )
14:12,13,11:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. A. x ( x e. A -> A. y e. C ph ) ).
15:14:	|- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ->. A. x e. A A. y e. C ph ).
16:15:	|- (. ( A C_ B /\ C C_ D ) ->. ( A. x e. B A. y e. D ph -> A. x e. A A. y e. C ph ) ).
qed:16:	|- ( ( A C_ B /\ C C_ D ) -> ( A. x e. B A. y e. D ph -> A. x e. A A. y e. C ph ) )

(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A C_ B /\ C C_ D ) -> ( A. x e. B A. y e. D ph -> A. x e. A A. y e. C ph ) )

Theorem

ordelordALTVD 36698

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5432 using the Axiom of Regularity indirectly through dford2 8070. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that _E Fr A because this is inferred by the Axiom of Regularity. 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. ordelordALT 36328 is ordelordALTVD 36698 without virtual deductions and was automatically derived from ordelordALTVD 36698 using the tools program translate..without..overwriting.cmd and Metamath's minimize command.

1::	|- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ).
2:1:	|- (. ( Ord A /\ B e. A ) ->. Ord A ).
3:1:	|- (. ( Ord A /\ B e. A ) ->. B e. A ).
4:2:	|- (. ( Ord A /\ B e. A ) ->. Tr A ).
5:2:	|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ).
6:4,3:	|- (. ( Ord A /\ B e. A ) ->. B C_ A ).
7:6,6,5:	|- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ).
8::	|- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
9:8:	|- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
10:9:	|- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
11:10:	|- ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
12:11:	|- A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
13:12:	|- A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
14:13:	|- ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
15:14,5:	|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
16:4,15,3:	|- (. ( Ord A /\ B e. A ) ->. Tr B ).
17:16,7:	|- (. ( Ord A /\ B e. A ) ->. Ord B ).
qed:17:	|- ( ( Ord A /\ B e. A ) -> Ord B )

(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( Ord A /\ B e. A ) -> Ord B )

Theorem

equncomVD 36699

If a class equals the union of two other classes, then it equals the union of those two classes commuted. 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. equncom 3588 is equncomVD 36699 without virtual deductions and was automatically derived from equncomVD 36699.

1::	|- (. A = ( B u. C ) ->. A = ( B u. C ) ).
2::	|- ( B u. C ) = ( C u. B )
3:1,2:	|- (. A = ( B u. C ) ->. A = ( C u. B ) ).
4:3:	|- ( A = ( B u. C ) -> A = ( C u. B ) )
5::	|- (. A = ( C u. B ) ->. A = ( C u. B ) ).
6:5,2:	|- (. A = ( C u. B ) ->. A = ( B u. C ) ).
7:6:	|- ( A = ( C u. B ) -> A = ( B u. C ) )
8:4,7:	|- ( A = ( B u. C ) <-> A = ( C u. B ) )

(Contributed by Alan Sare, 17-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A = ( B u. C ) <-> A = ( C u. B ) )

Theorem

equncomiVD 36700

Inference form of equncom 3588. 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 3589 is equncomiVD 36700 without virtual deductions and was automatically derived from equncomiVD 36700.

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.)

|- A = ( B u. C )   =>    |- A = ( C u. B )