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  4350  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  ctssdccl  7170  onntri35  7297  dftap2  7311  ltexnqq  7468  enq0tr  7494  prarloc  7563  addclpr  7597  nqprxx  7606  mulclpr  7632  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  caucvgprlemcl  7736  caucvgprprlemcl  7764  suplocexprlemex  7782  mpomulf  8009  le2tri3i  8128  ltmul1  8611  nn0ge2m1nn  9300  difgtsumgt  9386  nn0ge0div  9404  eluzp1p1  9618  peano2uz  9648  zgt1rpn0n1  9761  ledivge1le  9792  elioc2  10002  elico2  10003  elicc2  10004  iccsupr  10032  elfzd  10082  uzsubsubfz  10113  fzrev3  10153  elfz1b  10156  fseq1p1m1  10160  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzmlbp  10198  elfzo2  10216  elfzo0  10249  fzo1fzo0n0  10250  elfzo0z  10251  fzofzim  10255  elfzo1  10257  ubmelfzo  10267  elfzodifsumelfzo  10268  elfzom1elp1fzo  10269  fzossfzop1  10279  ssfzo12bi  10292  subfzo0  10309  fldiv4p1lem1div2  10374  intqfrac2  10390  intfracq  10391  modfzo0difsn  10466  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemstep  10585  seqf1oglem2  10591  wrdlenge2n0  10949  remullem  11015  qdenre  11346  maxabslemval  11352  xrmaxiflemval  11393  summodclem2a  11524  fsum3  11530  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  sumsplitdc  11575  fsummulc2  11591  isumlessdc  11639  prodmodclem3  11718  prodmodclem2a  11719  prodmodclem2  11720  prodmodc  11721  fprodeq0  11760  sin02gt0  11907  p1modz1  11937  divconjdvds  11991  addmodlteqALT  12001  ltoddhalfle  12034  4dvdseven  12058  dfgcd2  12151  rppwr  12165  qredeq  12234  divgcdcoprmex  12240  cncongr1  12241  dvdsnprmd  12263  oddprmge3  12273  isprm5  12280  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem19  12420  difsqpwdvds  12476  oddprmdvds  12492  ennnfoneleminc  12568  ctinf  12587  ssomct  12602  sgrpidmndm  13001  idmhm  13041  mhmf1o  13042  insubm  13057  0mhm  13058  resmhm  13059  resmhm2  13060  resmhm2b  13061  mhmco  13062  grpinvid1  13124  grpinvid2  13125  grplcan  13134  dfgrp3m  13171  dfgrp3me  13172  mhmfmhm  13187  issubg2m  13259  issubg4m  13263  ghmmhm  13323  rngrz  13442  srglmhm  13489  srgrmhm  13490  ringlz  13539  ringrz  13540  ringinvnzdiv  13546  ring1  13555  unitgrp  13612  isrhm2d  13661  subrgunit  13735  issubrg2  13737  islmodd  13789  dflidl2rng  13977  rnglidlmmgm  13992  quscrng  14029  upxp  14440  bdmopn  14672  suplociccex  14779  ivthreinc  14799  ptolemy  14959  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  dceqnconst  15550  dcapnconst  15551