Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpid3g
Next ⟩
ifpid2g
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpid3g
Description:
Restate wff as conditional logic operator.
(Contributed by
RP
, 20-Apr-2020)
Ref
Expression
Assertion
ifpid3g
⊢
χ
↔
if-
φ
ψ
χ
↔
φ
∧
ψ
→
χ
∧
φ
∧
χ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
olc
⊢
χ
→
φ
∨
χ
2
1
1
pm3.2i
⊢
χ
→
φ
∨
χ
∧
χ
→
φ
∨
χ
3
ifpidg
⊢
χ
↔
if-
φ
ψ
χ
↔
φ
∧
ψ
→
χ
∧
φ
∧
χ
→
ψ
∧
χ
→
φ
∨
χ
∧
χ
→
φ
∨
χ
4
2
3
mpbiran2
⊢
χ
↔
if-
φ
ψ
χ
↔
φ
∧
ψ
→
χ
∧
φ
∧
χ
→
ψ