This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus The conditional operator for propositions ifpbi123d
Description: Equivalence deduction for conditional operator for propositions.
(Contributed by AV , 30-Dec-2020) (Proof shortened by Wolf Lammen , 17-Apr-2024)
Ref
Expression
Hypotheses
ifpbi123d.1 ⊢ φ → ψ ↔ τ
ifpbi123d.2 ⊢ φ → χ ↔ η
ifpbi123d.3 ⊢ φ → θ ↔ ζ
Assertion
ifpbi123d ⊢ φ → if- ψ χ θ ↔ if- τ η ζ
Proof
Step
Hyp
Ref
Expression
1
ifpbi123d.1 ⊢ φ → ψ ↔ τ
2
ifpbi123d.2 ⊢ φ → χ ↔ η
3
ifpbi123d.3 ⊢ φ → θ ↔ ζ
4
1 2
imbi12d ⊢ φ → ψ → χ ↔ τ → η
5
1 3
orbi12d ⊢ φ → ψ ∨ θ ↔ τ ∨ ζ
6
4 5
anbi12d ⊢ φ → ψ → χ ∧ ψ ∨ θ ↔ τ → η ∧ τ ∨ ζ
7
dfifp3 ⊢ if- ψ χ θ ↔ ψ → χ ∧ ψ ∨ θ
8
dfifp3 ⊢ if- τ η ζ ↔ τ → η ∧ τ ∨ ζ
9
6 7 8
3bitr4g ⊢ φ → if- ψ χ θ ↔ if- τ η ζ