Metamath Proof Explorer

Theorem ensymd

Description: Symmetry of equinumerosity. Deduction form of ensym . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypothesis ensymd.1 
|- ( ph -> A ~~ B )
Assertion ensymd 
|- ( ph -> B ~~ A )

Proof

Step Hyp Ref Expression
1 ensymd.1 
 |-  ( ph -> A ~~ B )
2 ensym 
 |-  ( A ~~ B -> B ~~ A )
3 1 2 syl 
 |-  ( ph -> B ~~ A )