Metamath Proof Explorer

Theorem 3anbi2i

Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006)

Ref Expression
Hypothesis 3anbi1i.1 
|- ( ph <-> ps )
Assertion 3anbi2i 
|- ( ( ch /\ ph /\ th ) <-> ( ch /\ ps /\ th ) )

Proof

Step Hyp Ref Expression
1 3anbi1i.1 
 |-  ( ph <-> ps )
2 biid 
 |-  ( ch <-> ch )
3 biid 
 |-  ( th <-> th )
4 2 1 3 3anbi123i 
 |-  ( ( ch /\ ph /\ th ) <-> ( ch /\ ps /\ th ) )