Metamath Proof Explorer

Theorem 3anim1i

Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009)

Ref Expression
Hypothesis 3animi.1 φ ψ
Assertion 3anim1i φ χ θ ψ χ θ


Step Hyp Ref Expression
1 3animi.1 φ ψ
2 id χ χ
3 id θ θ
4 1 2 3 3anim123i φ χ θ ψ χ θ