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θψχ