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 ]. E. b e. B E. c e. C E. d e. D E. e e. E ph <-> E. b e. B E. c e. C E. d e. D E. e e. E [. A / a ]. ph )

Proof

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