Theorem 3anim123i 1181

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 1017	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1018	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1019	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1176	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  3anim1i  1182  3anim2i  1183  3anim3i  1184  syl3an  1270  syl3anl  1279  spc3egv  3198  eloprabga  6388  le2tri3i  9731  fzmmmeqm  11742  elfz1b  11773  elfz0fzfz0  11804  elfzmlbmOLD  11810  elfzmlbp  11811  elfzo1  11869  ssfzoulel  11908  flltdivnn0lt  11967  swrdswrd  12696  swrdccatin2  12723  swrdccat  12729  mulmoddvds  14055  symg2hash  16548  pmtrdifellem2  16628  unitgrp  17442  isdrngd  17547  bcthlem5  21892  colinearalg  24339  axcontlem8  24400  usgra2adedgwlk  24740  rngosn  25532  chirredlem2  27436  rexdiv  27774  nnssi2  30082  nnssi3  30083  isdrngo2  30523  expgrowthi  31400  el2fzo  32561  2zrngasgrp  32848  2zrngmsgrp  32855  lincvalpr  33121  bnj944  34097  bnj969  34105  leatb  35118  paddasslem9  35653  paddasslem10  35654  dvhvaddass  36925