Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpan123g
Next ⟩
ifpan23
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpan123g
Description:
Conjunction of conditional logical operators.
(Contributed by
RP
, 18-Apr-2020)
Ref
Expression
Assertion
ifpan123g
⊢
if-
φ
χ
τ
∧
if-
ψ
θ
η
↔
¬
φ
∨
χ
∧
φ
∨
τ
∧
¬
ψ
∨
θ
∧
ψ
∨
η
Proof
Step
Hyp
Ref
Expression
1
dfifp4
⊢
if-
φ
χ
τ
↔
¬
φ
∨
χ
∧
φ
∨
τ
2
dfifp4
⊢
if-
ψ
θ
η
↔
¬
ψ
∨
θ
∧
ψ
∨
η
3
1
2
anbi12i
⊢
if-
φ
χ
τ
∧
if-
ψ
θ
η
↔
¬
φ
∨
χ
∧
φ
∨
τ
∧
¬
ψ
∨
θ
∧
ψ
∨
η