Metamath Proof Explorer

Theorem bigolden

Description: Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005)

Ref Expression
Assertion bigolden 
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )

Proof

Step Hyp Ref Expression
1 pm4.71 
 |-  ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
2 pm4.72 
 |-  ( ( ph -> ps ) <-> ( ps <-> ( ph \/ ps ) ) )
3 bicom 
 |-  ( ( ph <-> ( ph /\ ps ) ) <-> ( ( ph /\ ps ) <-> ph ) )
4 1 2 3 3bitr3ri 
 |-  ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )