Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifporcor
Next ⟩
ifpdfan2
Metamath Proof Explorer
Ascii
Unicode
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-
ψ
ψ
φ