Theorem 3anim123i

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

	Ref	Expression
Hypotheses	3anim123i.1	|- ( ph -> ps )
	3anim123i.2	|- ( ch -> th )
	3anim123i.3	|- ( ta -> et )
Assertion	3anim123i	|- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Proof

Step	Hyp	Ref	Expression
1		3anim123i.1	|- ( ph -> ps )
2		3anim123i.2	|- ( ch -> th )
3		3anim123i.3	|- ( ta -> et )
4	1	3ad2ant1	|- ( ( ph /\ ch /\ ta ) -> ps )
5	2	3ad2ant2	|- ( ( ph /\ ch /\ ta ) -> th )
6	3	3ad2ant3	|- ( ( ph /\ ch /\ ta ) -> et )
7	4 5 6	3jca	|- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )