Metamath Proof Explorer

Theorem redundpbi1

Description: Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022)

Ref Expression
Hypothesis redundpbi1.1 ⊢ φ ↔ θ
Assertion redundpbi1 ⊢ redund φ ψ χ ↔ redund θ ψ χ

Proof

Step Hyp Ref Expression
1 redundpbi1.1 ⊢ φ ↔ θ
2 1 imbi1i ⊢ φ → ψ ↔ θ → ψ
3 1 anbi1i ⊢ φ ∧ χ ↔ θ ∧ χ
4 3 bibi1i ⊢ φ ∧ χ ↔ ψ ∧ χ ↔ θ ∧ χ ↔ ψ ∧ χ
5 2 4 anbi12i ⊢ φ → ψ ∧ φ ∧ χ ↔ ψ ∧ χ ↔ θ → ψ ∧ θ ∧ χ ↔ ψ ∧ χ
6 df-redundp ⊢ redund φ ψ χ ↔ φ → ψ ∧ φ ∧ χ ↔ ψ ∧ χ
7 df-redundp ⊢ redund θ ψ χ ↔ θ → ψ ∧ θ ∧ χ ↔ ψ ∧ χ
8 5 6 7 3bitr4i ⊢ redund φ ψ χ ↔ redund θ ψ χ