Metamath Proof Explorer

Theorem bicomd

Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993)

Ref Expression
Hypothesis bicomd.1 
|- ( ph -> ( ps <-> ch ) )
Assertion bicomd 
|- ( ph -> ( ch <-> ps ) )

Proof

Step Hyp Ref Expression
1 bicomd.1 
 |-  ( ph -> ( ps <-> ch ) )
2 bicom 
 |-  ( ( ps <-> ch ) <-> ( ch <-> ps ) )
3 1 2 sylib 
 |-  ( ph -> ( ch <-> ps ) )