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

Metamath Proof Explorer

Theorem 3anbi3d

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006)

Ref Expression
Hypothesis 3anbi1d.1 
|- ( ph -> ( ps <-> ch ) )
Assertion 3anbi3d 
|- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 3anbi1d.1 
 |-  ( ph -> ( ps <-> ch ) )
2 biidd 
 |-  ( ph -> ( th <-> th ) )
3 2 1 3anbi13d 
 |-  ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )