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 φ ψ
Assertion 3anbi2i χ φ θ χ ψ θ


Step Hyp Ref Expression
1 3anbi1i.1 φ ψ
2 biid χ χ
3 biid θ θ
4 2 1 3 3anbi123i χ φ θ χ ψ θ