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  4355  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  ctssdccl  7186  onntri35  7322  dftap2  7336  ltexnqq  7494  enq0tr  7520  prarloc  7589  addclpr  7623  nqprxx  7632  mulclpr  7658  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  caucvgprlemcl  7762  caucvgprprlemcl  7790  suplocexprlemex  7808  mpomulf  8035  le2tri3i  8154  ltmul1  8638  nn0ge2m1nn  9328  difgtsumgt  9414  nn0ge0div  9432  eluzp1p1  9646  peano2uz  9676  zgt1rpn0n1  9789  ledivge1le  9820  elioc2  10030  elico2  10031  elicc2  10032  iccsupr  10060  elfzd  10110  uzsubsubfz  10141  fzrev3  10181  elfz1b  10184  fseq1p1m1  10188  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzmlbp  10226  elfzo2  10244  elfzo0  10277  fzo1fzo0n0  10278  elfzo0z  10279  fzofzim  10283  elfzo1  10285  ubmelfzo  10295  elfzodifsumelfzo  10296  elfzom1elp1fzo  10297  fzossfzop1  10307  ssfzo12bi  10320  subfzo0  10337  fldiv4p1lem1div2  10414  intqfrac2  10430  intfracq  10431  modfzo0difsn  10506  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemstep  10625  seqf1oglem2  10631  wrdlenge2n0  10989  remullem  11055  qdenre  11386  maxabslemval  11392  xrmaxiflemval  11434  summodclem2a  11565  fsum3  11571  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  sumsplitdc  11616  fsummulc2  11632  isumlessdc  11680  prodmodclem3  11759  prodmodclem2a  11760  prodmodclem2  11761  prodmodc  11762  fprodeq0  11801  sin02gt0  11948  p1modz1  11978  divconjdvds  12033  addmodlteqALT  12043  ltoddhalfle  12077  4dvdseven  12101  dfgcd2  12208  rppwr  12222  qredeq  12291  divgcdcoprmex  12297  cncongr1  12298  dvdsnprmd  12320  oddprmge3  12330  isprm5  12337  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem19  12478  difsqpwdvds  12534  oddprmdvds  12550  ennnfoneleminc  12655  ctinf  12674  ssomct  12689  sgrpidmndm  13124  idmhm  13173  mhmf1o  13174  insubm  13189  0mhm  13190  resmhm  13191  resmhm2  13192  resmhm2b  13193  mhmco  13194  grpinvid1  13256  grpinvid2  13257  grplcan  13266  dfgrp3m  13303  dfgrp3me  13304  mhmfmhm  13325  issubg2m  13397  issubg4m  13401  ghmmhm  13461  rngrz  13580  srglmhm  13627  srgrmhm  13628  ringlz  13677  ringrz  13678  ringinvnzdiv  13684  ring1  13693  unitgrp  13750  isrhm2d  13799  subrgunit  13873  issubrg2  13875  islmodd  13927  dflidl2rng  14115  rnglidlmmgm  14130  quscrng  14167  upxp  14616  bdmopn  14848  suplociccex  14969  ivthreinc  14989  ptolemy  15168  perfectlem1  15343  gausslemma2dlem1a  15407  gausslemma2dlem4  15413  dceqnconst  15817  dcapnconst  15818