Theorem 3anim123i 1128

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

Hypotheses

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

Assertion

Ref	Expression
3anim123i	|- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Proof of Theorem 3anim123i

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

Syntax hints:   -> wi 4   /\ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  3anim1i  1129  3anim2i  1130  3anim3i  1131  syl3an  1216  syl3anl  1225  spc3egv  2710  spc3gv  2711  eloprabga  5735  le2tri3i  7591  fzmmmeqm  9469  elfz1b  9500  elfz0fzfz0  9533  elfzmlbp  9539  elfzo1  9597  flltdivnn0lt  9707  modmulconst  11102  nndvdslegcd  11231