Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpor123g
Next ⟩
ifpimim
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpor123g
Description:
Disjunction of conditional logical operators.
(Contributed by
RP
, 18-Apr-2020)
Ref
Expression
Assertion
ifpor123g
⊢
if-
φ
χ
τ
∨
if-
ψ
θ
η
↔
φ
→
¬
ψ
∨
χ
∨
θ
∧
ψ
→
φ
∨
τ
∨
θ
∧
φ
→
ψ
∨
χ
∨
η
∧
¬
ψ
→
φ
∨
τ
∨
η
Proof
Step
Hyp
Ref
Expression
1
df-or
⊢
if-
φ
χ
τ
∨
if-
ψ
θ
η
↔
¬
if-
φ
χ
τ
→
if-
ψ
θ
η
2
ifpnot23
⊢
¬
if-
φ
χ
τ
↔
if-
φ
¬
χ
¬
τ
3
2
imbi1i
⊢
¬
if-
φ
χ
τ
→
if-
ψ
θ
η
↔
if-
φ
¬
χ
¬
τ
→
if-
ψ
θ
η
4
1
3
bitri
⊢
if-
φ
χ
τ
∨
if-
ψ
θ
η
↔
if-
φ
¬
χ
¬
τ
→
if-
ψ
θ
η
5
ifpim123g
⊢
if-
φ
¬
χ
¬
τ
→
if-
ψ
θ
η
↔
φ
→
¬
ψ
∨
¬
χ
→
θ
∧
ψ
→
φ
∨
¬
τ
→
θ
∧
φ
→
ψ
∨
¬
χ
→
η
∧
¬
ψ
→
φ
∨
¬
τ
→
η
6
4
5
bitri
⊢
if-
φ
χ
τ
∨
if-
ψ
θ
η
↔
φ
→
¬
ψ
∨
¬
χ
→
θ
∧
ψ
→
φ
∨
¬
τ
→
θ
∧
φ
→
ψ
∨
¬
χ
→
η
∧
¬
ψ
→
φ
∨
¬
τ
→
η
7
pm4.64
⊢
¬
χ
→
θ
↔
χ
∨
θ
8
7
orbi2i
⊢
φ
→
¬
ψ
∨
¬
χ
→
θ
↔
φ
→
¬
ψ
∨
χ
∨
θ
9
pm4.64
⊢
¬
τ
→
θ
↔
τ
∨
θ
10
9
orbi2i
⊢
ψ
→
φ
∨
¬
τ
→
θ
↔
ψ
→
φ
∨
τ
∨
θ
11
8
10
anbi12i
⊢
φ
→
¬
ψ
∨
¬
χ
→
θ
∧
ψ
→
φ
∨
¬
τ
→
θ
↔
φ
→
¬
ψ
∨
χ
∨
θ
∧
ψ
→
φ
∨
τ
∨
θ
12
pm4.64
⊢
¬
χ
→
η
↔
χ
∨
η
13
12
orbi2i
⊢
φ
→
ψ
∨
¬
χ
→
η
↔
φ
→
ψ
∨
χ
∨
η
14
pm4.64
⊢
¬
τ
→
η
↔
τ
∨
η
15
14
orbi2i
⊢
¬
ψ
→
φ
∨
¬
τ
→
η
↔
¬
ψ
→
φ
∨
τ
∨
η
16
13
15
anbi12i
⊢
φ
→
ψ
∨
¬
χ
→
η
∧
¬
ψ
→
φ
∨
¬
τ
→
η
↔
φ
→
ψ
∨
χ
∨
η
∧
¬
ψ
→
φ
∨
τ
∨
η
17
11
16
anbi12i
⊢
φ
→
¬
ψ
∨
¬
χ
→
θ
∧
ψ
→
φ
∨
¬
τ
→
θ
∧
φ
→
ψ
∨
¬
χ
→
η
∧
¬
ψ
→
φ
∨
¬
τ
→
η
↔
φ
→
¬
ψ
∨
χ
∨
θ
∧
ψ
→
φ
∨
τ
∨
θ
∧
φ
→
ψ
∨
χ
∨
η
∧
¬
ψ
→
φ
∨
τ
∨
η
18
6
17
bitri
⊢
if-
φ
χ
τ
∨
if-
ψ
θ
η
↔
φ
→
¬
ψ
∨
χ
∨
θ
∧
ψ
→
φ
∨
τ
∨
θ
∧
φ
→
ψ
∨
χ
∨
η
∧
¬
ψ
→
φ
∨
τ
∨
η