Metamath Proof Explorer

Theorem 2sbcrex

Description: Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

Ref Expression
Assertion 2sbcrex 
|- ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )

Proof

Step Hyp Ref Expression
1 sbcrex 
 |-  ( [. B / b ]. E. c e. C ph <-> E. c e. C [. B / b ]. ph )
2 1 sbcbii 
 |-  ( [. A / a ]. [. B / b ]. E. c e. C ph <-> [. A / a ]. E. c e. C [. B / b ]. ph )
3 sbcrex 
 |-  ( [. A / a ]. E. c e. C [. B / b ]. ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )
4 2 3 bitri 
 |-  ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )