Theorem 3jca 1177

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

Hypotheses

Ref	Expression
3jca.1	|- ( ph -> ps )
3jca.2	|- ( ph -> ch )
3jca.3	|- ( ph -> th )

Assertion

Ref	Expression
3jca	|- ( ph -> ( ps /\ ch /\ th ) )

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 |- ( ph -> ps )
2		3jca.2	. . 3 |- ( ph -> ch )
3		3jca.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 309	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		df-3an 980	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 134	1 |- ( ph -> ( ps /\ ch /\ th ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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 980

This theorem is referenced by:  3jcad  1178  mpbir3and  1180  syl3anbrc  1181  3anim123i  1184  syl3anc  1238  syl13anc  1240  syl31anc  1241  syl113anc  1250  syl131anc  1251  syl311anc  1252  syl33anc  1253  syl133anc  1261  syl313anc  1262  syl331anc  1263  syl333anc  1270  3jaob  1302  mp3and  1340  issod  4317  tfrlemibxssdm  6323  tfr1onlembxssdm  6339  tfrcllembxssdm  6352  ctssdccl  7105  onntri35  7231  dftap2  7245  ltexnqq  7402  enq0tr  7428  prarloc  7497  addclpr  7531  nqprxx  7540  mulclpr  7566  ltexprlempr  7602  recexprlempr  7626  cauappcvgprlemcl  7647  caucvgprlemcl  7670  caucvgprprlemcl  7698  suplocexprlemex  7716  le2tri3i  8060  ltmul1  8543  nn0ge2m1nn  9230  difgtsumgt  9316  nn0ge0div  9334  eluzp1p1  9547  peano2uz  9577  zgt1rpn0n1  9689  ledivge1le  9720  elioc2  9930  elico2  9931  elicc2  9932  iccsupr  9960  uzsubsubfz  10040  fzrev3  10080  elfz1b  10083  fseq1p1m1  10087  elfz0ubfz0  10118  elfz0fzfz0  10119  fz0fzelfz0  10120  fz0fzdiffz0  10123  elfzmlbp  10125  elfzo2  10143  elfzo0  10175  fzo1fzo0n0  10176  elfzo0z  10177  fzofzim  10181  elfzo1  10183  ubmelfzo  10193  elfzodifsumelfzo  10194  elfzom1elp1fzo  10195  fzossfzop1  10205  ssfzo12bi  10218  subfzo0  10235  fldiv4p1lem1div2  10298  intqfrac2  10312  intfracq  10313  modfzo0difsn  10388  iseqf1olemqcl  10479  iseqf1olemnab  10481  iseqf1olemab  10482  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemstep  10494  remullem  10871  qdenre  11202  maxabslemval  11208  xrmaxiflemval  11249  summodclem2a  11380  fsum3  11386  fsum3cvg3  11395  fsumcl2lem  11397  fsumadd  11405  sumsplitdc  11431  fsummulc2  11447  isumlessdc  11495  prodmodclem3  11574  prodmodclem2a  11575  prodmodclem2  11576  prodmodc  11577  fprodeq0  11616  sin02gt0  11762  p1modz1  11792  divconjdvds  11845  addmodlteqALT  11855  ltoddhalfle  11888  4dvdseven  11912  dfgcd2  12005  rppwr  12019  qredeq  12086  divgcdcoprmex  12092  cncongr1  12093  dvdsnprmd  12115  oddprmge3  12125  isprm5  12132  pythagtriplem6  12260  pythagtriplem7  12261  pythagtriplem19  12272  difsqpwdvds  12327  oddprmdvds  12342  ennnfoneleminc  12402  ctinf  12421  ssomct  12436  sgrpidmndm  12751  idmhm  12788  mhmf1o  12789  insubm  12800  0mhm  12801  mhmco  12802  grpinvid1  12852  grpinvid2  12853  grplcan  12860  dfgrp3m  12897  dfgrp3me  12898  mhmfmhm  12909  issubg2m  12975  issubg4m  12979  srglmhm  13076  srgrmhm  13077  ringlz  13122  ringrz  13123  ringinvnzdiv  13127  ring1  13136  unitgrp  13184  upxp  13554  bdmopn  13786  suplociccex  13885  ptolemy  14027  dceqnconst  14578  dcapnconst  14579