Metamath Proof Explorer

Theorem redundpim3

Description: Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Hypothesis redundpim3.1 ${⊢}{\theta }\to {\chi }$
Assertion redundpim3 ${⊢}redund\left({\phi },{\psi },{\chi }\right)\to redund\left({\phi },{\psi },{\theta }\right)$

Proof

Step Hyp Ref Expression
1 redundpim3.1 ${⊢}{\theta }\to {\chi }$
2 anbi1 ${⊢}\left(\left({\phi }\wedge {\chi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\to \left(\left(\left({\phi }\wedge {\chi }\right)\wedge {\theta }\right)↔\left(\left({\psi }\wedge {\chi }\right)\wedge {\theta }\right)\right)$
3 1 pm4.71ri ${⊢}{\theta }↔\left({\chi }\wedge {\theta }\right)$
4 3 bianass ${⊢}\left({\phi }\wedge {\theta }\right)↔\left(\left({\phi }\wedge {\chi }\right)\wedge {\theta }\right)$
5 3 bianass ${⊢}\left({\psi }\wedge {\theta }\right)↔\left(\left({\psi }\wedge {\chi }\right)\wedge {\theta }\right)$
6 2 4 5 3bitr4g ${⊢}\left(\left({\phi }\wedge {\chi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\to \left(\left({\phi }\wedge {\theta }\right)↔\left({\psi }\wedge {\theta }\right)\right)$
7 6 anim2i ${⊢}\left(\left({\phi }\to {\psi }\right)\wedge \left(\left({\phi }\wedge {\chi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\right)\to \left(\left({\phi }\to {\psi }\right)\wedge \left(\left({\phi }\wedge {\theta }\right)↔\left({\psi }\wedge {\theta }\right)\right)\right)$
8 df-redundp ${⊢}redund\left({\phi },{\psi },{\chi }\right)↔\left(\left({\phi }\to {\psi }\right)\wedge \left(\left({\phi }\wedge {\chi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\right)$
9 df-redundp ${⊢}redund\left({\phi },{\psi },{\theta }\right)↔\left(\left({\phi }\to {\psi }\right)\wedge \left(\left({\phi }\wedge {\theta }\right)↔\left({\psi }\wedge {\theta }\right)\right)\right)$
10 7 8 9 3imtr4i ${⊢}redund\left({\phi },{\psi },{\chi }\right)\to redund\left({\phi },{\psi },{\theta }\right)$