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 ( 𝜃 , 𝜓 , 𝜒 ) )