Metamath Proof Explorer


Theorem 3anim123i

Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994)

Ref Expression
Hypotheses 3anim123i.1 φ ψ
3anim123i.2 χ θ
3anim123i.3 τ η
Assertion 3anim123i φ χ τ ψ θ η

Proof

Step Hyp Ref Expression
1 3anim123i.1 φ ψ
2 3anim123i.2 χ θ
3 3anim123i.3 τ η
4 1 3ad2ant1 φ χ τ ψ
5 2 3ad2ant2 φ χ τ θ
6 3 3ad2ant3 φ χ τ η
7 4 5 6 3jca φ χ τ ψ θ η