Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpbi13
Next ⟩
ifpbi123
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpbi13
Description:
Equivalence theorem for conditional logical operators.
(Contributed by
RP
, 15-Apr-2020)
Ref
Expression
Assertion
ifpbi13
⊢
φ
↔
ψ
∧
χ
↔
θ
→
if-
φ
τ
χ
↔
if-
ψ
τ
θ
Proof
Step
Hyp
Ref
Expression
1
simpl
⊢
φ
↔
ψ
∧
χ
↔
θ
→
φ
↔
ψ
2
1
imbi1d
⊢
φ
↔
ψ
∧
χ
↔
θ
→
φ
→
τ
↔
ψ
→
τ
3
notbi
⊢
φ
↔
ψ
↔
¬
φ
↔
¬
ψ
4
imbi12
⊢
¬
φ
↔
¬
ψ
→
χ
↔
θ
→
¬
φ
→
χ
↔
¬
ψ
→
θ
5
3
4
sylbi
⊢
φ
↔
ψ
→
χ
↔
θ
→
¬
φ
→
χ
↔
¬
ψ
→
θ
6
5
imp
⊢
φ
↔
ψ
∧
χ
↔
θ
→
¬
φ
→
χ
↔
¬
ψ
→
θ
7
2
6
anbi12d
⊢
φ
↔
ψ
∧
χ
↔
θ
→
φ
→
τ
∧
¬
φ
→
χ
↔
ψ
→
τ
∧
¬
ψ
→
θ
8
dfifp2
⊢
if-
φ
τ
χ
↔
φ
→
τ
∧
¬
φ
→
χ
9
dfifp2
⊢
if-
ψ
τ
θ
↔
ψ
→
τ
∧
¬
ψ
→
θ
10
7
8
9
3bitr4g
⊢
φ
↔
ψ
∧
χ
↔
θ
→
if-
φ
τ
χ
↔
if-
ψ
τ
θ