Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpdfan2
Next ⟩
ifpancor
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpdfan2
Description:
Define and with conditional logic operator.
(Contributed by
RP
, 25-Apr-2020)
Ref
Expression
Assertion
ifpdfan2
⊢
φ
∧
ψ
↔
if-
φ
ψ
φ
Proof
Step
Hyp
Ref
Expression
1
id
⊢
φ
→
φ
2
1
notnoti
⊢
¬
¬
φ
→
φ
3
2
biorfi
⊢
φ
∧
ψ
↔
φ
∧
ψ
∨
¬
φ
→
φ
4
dfifp6
⊢
if-
φ
ψ
φ
↔
φ
∧
ψ
∨
¬
φ
→
φ
5
3
4
bitr4i
⊢
φ
∧
ψ
↔
if-
φ
ψ
φ