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