Metamath Proof Explorer

Theorem ifporcor

Description: Corollary of commutation of or. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifporcor 
|- ( if- ( ph , ph , ps ) <-> if- ( ps , ps , ph ) )

Proof

Step Hyp Ref Expression
1 orcom 
 |-  ( ( ph \/ ps ) <-> ( ps \/ ph ) )
2 ifpdfor2 
 |-  ( ( ph \/ ps ) <-> if- ( ph , ph , ps ) )
3 ifpdfor2 
 |-  ( ( ps \/ ph ) <-> if- ( ps , ps , ph ) )
4 1 2 3 3bitr3i 
 |-  ( if- ( ph , ph , ps ) <-> if- ( ps , ps , ph ) )