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  7320  dftap2  7334  ltexnqq  7492  enq0tr  7518  prarloc  7587  addclpr  7621  nqprxx  7630  mulclpr  7656  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  caucvgprlemcl  7760  caucvgprprlemcl  7788  suplocexprlemex  7806  mpomulf  8033  le2tri3i  8152  ltmul1  8636  nn0ge2m1nn  9326  difgtsumgt  9412  nn0ge0div  9430  eluzp1p1  9644  peano2uz  9674  zgt1rpn0n1  9787  ledivge1le  9818  elioc2  10028  elico2  10029  elicc2  10030  iccsupr  10058  elfzd  10108  uzsubsubfz  10139  fzrev3  10179  elfz1b  10182  fseq1p1m1  10186  elfz0ubfz0  10217  elfz0fzfz0  10218  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzmlbp  10224  elfzo2  10242  elfzo0  10275  fzo1fzo0n0  10276  elfzo0z  10277  fzofzim  10281  elfzo1  10283  ubmelfzo  10293  elfzodifsumelfzo  10294  elfzom1elp1fzo  10295  fzossfzop1  10305  ssfzo12bi  10318  subfzo0  10335  fldiv4p1lem1div2  10412  intqfrac2  10428  intfracq  10429  modfzo0difsn  10504  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemstep  10623  seqf1oglem2  10629  wrdlenge2n0  10987  remullem  11053  qdenre  11384  maxabslemval  11390  xrmaxiflemval  11432  summodclem2a  11563  fsum3  11569  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  sumsplitdc  11614  fsummulc2  11630  isumlessdc  11678  prodmodclem3  11757  prodmodclem2a  11758  prodmodclem2  11759  prodmodc  11760  fprodeq0  11799  sin02gt0  11946  p1modz1  11976  divconjdvds  12031  addmodlteqALT  12041  ltoddhalfle  12075  4dvdseven  12099  dfgcd2  12206  rppwr  12220  qredeq  12289  divgcdcoprmex  12295  cncongr1  12296  dvdsnprmd  12318  oddprmge3  12328  isprm5  12335  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem19  12476  difsqpwdvds  12532  oddprmdvds  12548  ennnfoneleminc  12653  ctinf  12672  ssomct  12687  sgrpidmndm  13122  idmhm  13171  mhmf1o  13172  insubm  13187  0mhm  13188  resmhm  13189  resmhm2  13190  resmhm2b  13191  mhmco  13192  grpinvid1  13254  grpinvid2  13255  grplcan  13264  dfgrp3m  13301  dfgrp3me  13302  mhmfmhm  13323  issubg2m  13395  issubg4m  13399  ghmmhm  13459  rngrz  13578  srglmhm  13625  srgrmhm  13626  ringlz  13675  ringrz  13676  ringinvnzdiv  13682  ring1  13691  unitgrp  13748  isrhm2d  13797  subrgunit  13871  issubrg2  13873  islmodd  13925  dflidl2rng  14113  rnglidlmmgm  14128  quscrng  14165  upxp  14592  bdmopn  14824  suplociccex  14945  ivthreinc  14965  ptolemy  15144  perfectlem1  15319  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  dceqnconst  15791  dcapnconst  15792