Metamath Proof Explorer


Theorem ifporcor

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

Ref Expression
Assertion ifporcor if- φ φ ψ if- ψ ψ φ

Proof

Step Hyp Ref Expression
1 orcom φ ψ ψ φ
2 ifpdfor2 φ ψ if- φ φ ψ
3 ifpdfor2 ψ φ if- ψ ψ φ
4 1 2 3 3bitr3i if- φ φ ψ if- ψ ψ φ