Metamath Proof Explorer


Theorem sbc4rex

Description: Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

Ref Expression
Assertion sbc4rex [˙A/a]˙bBcCdDeEφbBcCdDeE[˙A/a]˙φ

Proof

Step Hyp Ref Expression
1 sbc2rex [˙A/a]˙bBcCdDeEφbBcC[˙A/a]˙dDeEφ
2 sbc2rex [˙A/a]˙dDeEφdDeE[˙A/a]˙φ
3 2 2rexbii bBcC[˙A/a]˙dDeEφbBcCdDeE[˙A/a]˙φ
4 1 3 bitri [˙A/a]˙bBcCdDeEφbBcCdDeE[˙A/a]˙φ