This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj206

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj206.1 
|- ( ph' <-> [. M / n ]. ph )
bnj206.2 
|- ( ps' <-> [. M / n ]. ps )
bnj206.3 
|- ( ch' <-> [. M / n ]. ch )
bnj206.4 
|- M e. _V
Assertion bnj206 
|- ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )

Proof

Step Hyp Ref Expression
1 bnj206.1 
 |-  ( ph' <-> [. M / n ]. ph )
2 bnj206.2 
 |-  ( ps' <-> [. M / n ]. ps )
3 bnj206.3 
 |-  ( ch' <-> [. M / n ]. ch )
4 bnj206.4 
 |-  M e. _V
5 sbc3an 
 |-  ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( [. M / n ]. ph /\ [. M / n ]. ps /\ [. M / n ]. ch ) )
6 1 bicomi 
 |-  ( [. M / n ]. ph <-> ph' )
7 2 bicomi 
 |-  ( [. M / n ]. ps <-> ps' )
8 3 bicomi 
 |-  ( [. M / n ]. ch <-> ch' )
9 6 7 8 3anbi123i 
 |-  ( ( [. M / n ]. ph /\ [. M / n ]. ps /\ [. M / n ]. ch ) <-> ( ph' /\ ps' /\ ch' ) )
10 5 9 bitri 
 |-  ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )