Metamath Proof Explorer

Theorem sban

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 . (Contributed by NM, 14-May-1993) (Proof shortened by Steven Nguyen, 13-Aug-2023)

Ref Expression
Assertion sban ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)↔\left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)$

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
2 1 sbimi ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)\to \left[{y}/{x}\right]{\phi }$
3 simpr ${⊢}\left({\phi }\wedge {\psi }\right)\to {\psi }$
4 3 sbimi ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)\to \left[{y}/{x}\right]{\psi }$
5 2 4 jca ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)\to \left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)$
6 pm3.2 ${⊢}{\phi }\to \left({\psi }\to \left({\phi }\wedge {\psi }\right)\right)$
7 6 sb2imi ${⊢}\left[{y}/{x}\right]{\phi }\to \left(\left[{y}/{x}\right]{\psi }\to \left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)\right)$
8 7 imp ${⊢}\left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)\to \left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)$
9 5 8 impbii ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)↔\left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)$