Theorem 3jca 1179

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 982	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 134	1 |- ( ph -> ( ps /\ ch /\ th ) )

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

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 982

This theorem is referenced by:  3jcad  1180  mpbir3and  1182  syl3anbrc  1183  3anim123i  1186  syl3anc  1249  syl13anc  1251  syl31anc  1252  syl113anc  1261  syl131anc  1262  syl311anc  1263  syl33anc  1264  syl133anc  1272  syl313anc  1273  syl331anc  1274  syl333anc  1281  3jaob  1313  mp3and  1351  issod  4354  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  ctssdccl  7177  onntri35  7304  dftap2  7318  ltexnqq  7475  enq0tr  7501  prarloc  7570  addclpr  7604  nqprxx  7613  mulclpr  7639  ltexprlempr  7675  recexprlempr  7699  cauappcvgprlemcl  7720  caucvgprlemcl  7743  caucvgprprlemcl  7771  suplocexprlemex  7789  mpomulf  8016  le2tri3i  8135  ltmul1  8619  nn0ge2m1nn  9309  difgtsumgt  9395  nn0ge0div  9413  eluzp1p1  9627  peano2uz  9657  zgt1rpn0n1  9770  ledivge1le  9801  elioc2  10011  elico2  10012  elicc2  10013  iccsupr  10041  elfzd  10091  uzsubsubfz  10122  fzrev3  10162  elfz1b  10165  fseq1p1m1  10169  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzmlbp  10207  elfzo2  10225  elfzo0  10258  fzo1fzo0n0  10259  elfzo0z  10260  fzofzim  10264  elfzo1  10266  ubmelfzo  10276  elfzodifsumelfzo  10277  elfzom1elp1fzo  10278  fzossfzop1  10288  ssfzo12bi  10301  subfzo0  10318  fldiv4p1lem1div2  10395  intqfrac2  10411  intfracq  10412  modfzo0difsn  10487  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemstep  10606  seqf1oglem2  10612  wrdlenge2n0  10970  remullem  11036  qdenre  11367  maxabslemval  11373  xrmaxiflemval  11415  summodclem2a  11546  fsum3  11552  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  sumsplitdc  11597  fsummulc2  11613  isumlessdc  11661  prodmodclem3  11740  prodmodclem2a  11741  prodmodclem2  11742  prodmodc  11743  fprodeq0  11782  sin02gt0  11929  p1modz1  11959  divconjdvds  12014  addmodlteqALT  12024  ltoddhalfle  12058  4dvdseven  12082  dfgcd2  12181  rppwr  12195  qredeq  12264  divgcdcoprmex  12270  cncongr1  12271  dvdsnprmd  12293  oddprmge3  12303  isprm5  12310  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem19  12451  difsqpwdvds  12507  oddprmdvds  12523  ennnfoneleminc  12628  ctinf  12647  ssomct  12662  sgrpidmndm  13061  idmhm  13101  mhmf1o  13102  insubm  13117  0mhm  13118  resmhm  13119  resmhm2  13120  resmhm2b  13121  mhmco  13122  grpinvid1  13184  grpinvid2  13185  grplcan  13194  dfgrp3m  13231  dfgrp3me  13232  mhmfmhm  13247  issubg2m  13319  issubg4m  13323  ghmmhm  13383  rngrz  13502  srglmhm  13549  srgrmhm  13550  ringlz  13599  ringrz  13600  ringinvnzdiv  13606  ring1  13615  unitgrp  13672  isrhm2d  13721  subrgunit  13795  issubrg2  13797  islmodd  13849  dflidl2rng  14037  rnglidlmmgm  14052  quscrng  14089  upxp  14508  bdmopn  14740  suplociccex  14861  ivthreinc  14881  ptolemy  15060  perfectlem1  15235  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  dceqnconst  15704  dcapnconst  15705