Theorem eqcoms 813

Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.

Hypothesis

Ref	Expression
eqcoms.1	⊢ (x = y → φ)

Assertion

Ref	Expression
eqcoms	⊢ (y = x → φ)

ATD>eqcoms.1

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 811	. 2 ⊢ (y = x → x = y)
2		. 2 ⊢ (x = y → φ)
3	1, 2	syl 12	1 ⊢ (y = x → φ)

Syntax hints:   → wi 2   = weq 797

This theorem is referenced by:  eqt 814  eqt2b 818  a13b 819  a14b 820  eqvin.l1 851  sbequ12a 867  sbequi 876  sbequ 877  del45 879  sb5f1 917  sb6a 990  mo 1020  tfinds2 2405  eirrv 3449

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-8 798  ax-9 799  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org