Metamath Proof Explorer


Theorem sbc2rex

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

Ref Expression
Assertion sbc2rex [˙A / a]˙ b B c C φ b B c C [˙A / a]˙ φ

Proof

Step Hyp Ref Expression
1 sbcrex [˙A / a]˙ b B c C φ b B [˙A / a]˙ c C φ
2 sbcrex [˙A / a]˙ c C φ c C [˙A / a]˙ φ
3 2 rexbii b B [˙A / a]˙ c C φ b B c C [˙A / a]˙ φ
4 1 3 bitri [˙A / a]˙ b B c C φ b B c C [˙A / a]˙ φ