Theorem 3anim123i 1192

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 1028	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1029	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1030	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1187	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 984

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 189  df-an 373  df-3an 986

This theorem is referenced by:  3anim1i  1193  3anim2i  1194  3anim3i  1195  syl3an  1309  syl3anl  1318  spc3egv  3137  eloprabga  6380  le2tri3i  9761  fzmmmeqm  11829  elfz1b  11861  elfz0fzfz0  11892  elfzmlbmOLD  11898  elfzmlbp  11899  elfzo1  11962  ssfzoulel  12002  flltdivnn0lt  12062  swrdswrd  12811  swrdccatin2  12838  swrdccat  12844  mulmoddvds  14356  nndvdslegcd  14472  ncoprmlnprm  14670  symg2hash  17031  pmtrdifellem2  17111  unitgrp  17888  isdrngd  17993  bcthlem5  22289  colinearalg  24933  axcontlem8  24994  usgra2adedgwlk  25335  rngosn  26125  chirredlem2  28037  rexdiv  28388  bnj944  29742  bnj969  29750  nnssi2  31108  nnssi3  31109  isdrngo2  32190  leatb  32852  paddasslem9  33387  paddasslem10  33388  dvhvaddass  34659  expgrowthi  36676  nnsum4primesodd  38885  nnsum4primesoddALTV  38886  cplgr3v  39485  2zrngasgrp  39927  2zrngmsgrp  39934  lincvalpr  40198  refdivmptf  40340  refdivmptfv  40344