Theorem 3anim123i 1181

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

Hypotheses

Ref	Expression
3anim123i.1
3anim123i.2
3anim123i.3

Assertion

Ref	Expression
3anim123i

Proof of Theorem 3anim123i

Step	Hyp	Ref	Expression
1		3anim123i.1	. . 3
2	1	3ad2ant1 1017	. 2
3		3anim123i.2	. . 3
4	3	3ad2ant2 1018	. 2
5		3anim123i.3	. . 3
6	5	3ad2ant3 1019	. 2
7	2, 4, 6	3jca 1176	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  3anim1i  1182  3anim2i  1183  3anim3i  1184  syl3an  1270  syl3anl  1279  spc3egv  3198  eloprabga  6389  le2tri3i  9735  fzmmmeqm  11746  elfz1b  11777  elfz0fzfz0  11808  elfzmlbmOLD  11814  elfzmlbp  11815  elfzo1  11871  ssfzoulel  11906  flltdivnn0lt  11965  swrdspsleq  12673  swrdswrd  12685  swrdccatin2  12712  swrdccat  12718  mulmoddvds  14044  symg2hash  16422  pmtrdifellem2  16502  unitgrp  17316  isdrngd  17421  bcthlem5  21767  colinearalg  24213  axcontlem8  24274  usgra2adedgwlk  24614  rngosn  25406  chirredlem2  27310  rexdiv  27622  nnssi2  29920  nnssi3  29921  isdrngo2  30361  expgrowthi  31238  el2fzo  32339  2zrngasgrp  32746  2zrngmsgrp  32753  lincvalpr  33019  bnj944  33996  bnj969  34004  leatb  35017  paddasslem9  35552  paddasslem10  35553  dvhvaddass  36824

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