Theorem 3anim123i 1168

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 1004	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1005	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1006	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1163	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962

This theorem is referenced by:  3anim1i  1169  3anim3i  1170  syl3an  1255  syl3anl  1264  spc3egv  3058  eloprabga  6176  le2tri3i  9500  uzletr  10865  elfz0fzfz0  11481  elfzmlbm  11486  elfzmlbp  11487  fzmmmeqm  11488  elfz1b  11523  elfzo0z  11585  elfzo1  11591  ssfzoulel  11617  flltdivnn0lt  11673  swrdspsleq  12338  swrdswrd  12350  swrdccatin2  12374  swrdccat  12380  symg2hash  15895  pmtrdifellem2  15976  unitgrp  16749  isdrngd  16837  mdetunilem9  18326  bcthlem5  20739  colinearalg  23075  axcontlem8  23136  rngosn  23810  chirredlem2  25714  rexdiv  26018  nnssi2  28215  nnssi3  28216  welb  28539  isdrngo2  28673  expgrowthi  29516  uzuzle  30099  el2fzo  30121  mulmoddvds  30155  usgra2adedgwlk  30215  lincvalpr  30776  bnj944  31748  bnj969  31756  leatb  32625  paddasslem9  33160  paddasslem10  33161  dvhvaddass  34430