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 φχτψθη