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

Metamath Proof Explorer

Theorem bnj887

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj887.1 
|- ( ph <-> ph' )
bnj887.2 
|- ( ps <-> ps' )
bnj887.3 
|- ( ch <-> ch' )
bnj887.4 
|- ( th <-> th' )
Assertion bnj887 
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph' /\ ps' /\ ch' /\ th' ) )

Proof

Step Hyp Ref Expression
1 bnj887.1 
 |-  ( ph <-> ph' )
2 bnj887.2 
 |-  ( ps <-> ps' )
3 bnj887.3 
 |-  ( ch <-> ch' )
4 bnj887.4 
 |-  ( th <-> th' )
5 1 2 3 3anbi123i 
 |-  ( ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )
6 5 4 anbi12i 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) )
7 df-bnj17 
 |-  ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )
8 df-bnj17 
 |-  ( ( ph' /\ ps' /\ ch' /\ th' ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) )
9 6 7 8 3bitr4i 
 |-  ( ( ph /\ ps /\ ch /\ th ) <-> ( ph' /\ ps' /\ ch' /\ th' ) )