Description: Corollary of commutation of or. (Contributed by RP, 20-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ifporcor | ⊢ ( if- ( 𝜑 , 𝜑 , 𝜓 ) ↔ if- ( 𝜓 , 𝜓 , 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom | ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜓 ∨ 𝜑 ) ) | |
2 | ifpdfor2 | ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ if- ( 𝜑 , 𝜑 , 𝜓 ) ) | |
3 | ifpdfor2 | ⊢ ( ( 𝜓 ∨ 𝜑 ) ↔ if- ( 𝜓 , 𝜓 , 𝜑 ) ) | |
4 | 1 2 3 | 3bitr3i | ⊢ ( if- ( 𝜑 , 𝜑 , 𝜓 ) ↔ if- ( 𝜓 , 𝜓 , 𝜑 ) ) |