Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpimim
Next ⟩
ifpbibib
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpimim
Description:
Consequnce of implication.
(Contributed by
RP
, 17-Apr-2020)
Ref
Expression
Assertion
ifpimim
⊢
if-
φ
ψ
→
χ
θ
→
τ
→
if-
φ
ψ
θ
→
if-
φ
χ
τ
Proof
Step
Hyp
Ref
Expression
1
pm2.521
⊢
¬
¬
φ
→
φ
→
φ
→
¬
φ
2
1
orim1i
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
→
φ
→
¬
φ
∨
ψ
→
χ
3
2
adantr
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
¬
φ
∨
ψ
→
χ
4
id
⊢
φ
→
φ
5
4
orci
⊢
φ
→
φ
∨
θ
→
χ
6
5
a1i
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
φ
∨
θ
→
χ
7
3
6
jca
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
¬
φ
∨
ψ
→
χ
∧
φ
→
φ
∨
θ
→
χ
8
4
orci
⊢
φ
→
φ
∨
ψ
→
τ
9
8
a1i
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
φ
∨
ψ
→
τ
10
simpr
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
¬
φ
→
φ
∨
θ
→
τ
11
9
10
jca
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
φ
∨
ψ
→
τ
∧
¬
φ
→
φ
∨
θ
→
τ
12
7
11
jca
⊢
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
→
φ
→
¬
φ
∨
ψ
→
χ
∧
φ
→
φ
∨
θ
→
χ
∧
φ
→
φ
∨
ψ
→
τ
∧
¬
φ
→
φ
∨
θ
→
τ
13
pm4.81
⊢
¬
φ
→
φ
↔
φ
14
13
bicomi
⊢
φ
↔
¬
φ
→
φ
15
ifpbi1
⊢
φ
↔
¬
φ
→
φ
→
if-
φ
ψ
→
χ
θ
→
τ
↔
if-
¬
φ
→
φ
ψ
→
χ
θ
→
τ
16
14
15
ax-mp
⊢
if-
φ
ψ
→
χ
θ
→
τ
↔
if-
¬
φ
→
φ
ψ
→
χ
θ
→
τ
17
dfifp4
⊢
if-
¬
φ
→
φ
ψ
→
χ
θ
→
τ
↔
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
18
16
17
bitri
⊢
if-
φ
ψ
→
χ
θ
→
τ
↔
¬
¬
φ
→
φ
∨
ψ
→
χ
∧
¬
φ
→
φ
∨
θ
→
τ
19
ifpim123g
⊢
if-
φ
ψ
θ
→
if-
φ
χ
τ
↔
φ
→
¬
φ
∨
ψ
→
χ
∧
φ
→
φ
∨
θ
→
χ
∧
φ
→
φ
∨
ψ
→
τ
∧
¬
φ
→
φ
∨
θ
→
τ
20
12
18
19
3imtr4i
⊢
if-
φ
ψ
→
χ
θ
→
τ
→
if-
φ
ψ
θ
→
if-
φ
χ
τ