Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpdfor2
Next ⟩
ifporcor
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpdfor2
Description:
Define or in terms of conditional logic operator.
(Contributed by
RP
, 20-Apr-2020)
Ref
Expression
Assertion
ifpdfor2
⊢
φ
∨
ψ
↔
if-
φ
φ
ψ
Proof
Step
Hyp
Ref
Expression
1
pm2.1
⊢
¬
φ
∨
φ
2
1
biantrur
⊢
φ
∨
ψ
↔
¬
φ
∨
φ
∧
φ
∨
ψ
3
dfifp4
⊢
if-
φ
φ
ψ
↔
¬
φ
∨
φ
∧
φ
∨
ψ
4
2
3
bitr4i
⊢
φ
∨
ψ
↔
if-
φ
φ
ψ