Theorem 3anim123i 1208

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 1042	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1043	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1044	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1201	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  3anim1i  1209  3anim2i  1210  3anim3i  1211  syl3an  1313  syl3anl  1322  spc3egv  2895  spc3gv  2896  eloprabga  6091  le2tri3i  8255  fzmmmeqm  10254  elfz1b  10286  elfz0fzfz0  10322  elfzmlbp  10328  elfzo1  10391  flltdivnn0lt  10524  pfxeq  11228  swrdswrd  11237  swrdccat  11267  modmulconst  12334  nndvdslegcd  12486  lgsmulsqcoprm  15725