Metamath Proof Explorer


Theorem 3anbi3i

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

Ref Expression
Hypothesis 3anbi1i.1 φ ψ
Assertion 3anbi3i χ θ φ χ θ ψ

Proof

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