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  4321  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  ctssdccl  7112  onntri35  7238  dftap2  7252  ltexnqq  7409  enq0tr  7435  prarloc  7504  addclpr  7538  nqprxx  7547  mulclpr  7573  ltexprlempr  7609  recexprlempr  7633  cauappcvgprlemcl  7654  caucvgprlemcl  7677  caucvgprprlemcl  7705  suplocexprlemex  7723  le2tri3i  8068  ltmul1  8551  nn0ge2m1nn  9238  difgtsumgt  9324  nn0ge0div  9342  eluzp1p1  9555  peano2uz  9585  zgt1rpn0n1  9697  ledivge1le  9728  elioc2  9938  elico2  9939  elicc2  9940  iccsupr  9968  elfzd  10018  uzsubsubfz  10049  fzrev3  10089  elfz1b  10092  fseq1p1m1  10096  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  elfzmlbp  10134  elfzo2  10152  elfzo0  10184  fzo1fzo0n0  10185  elfzo0z  10186  fzofzim  10190  elfzo1  10192  ubmelfzo  10202  elfzodifsumelfzo  10203  elfzom1elp1fzo  10204  fzossfzop1  10214  ssfzo12bi  10227  subfzo0  10244  fldiv4p1lem1div2  10307  intqfrac2  10321  intfracq  10322  modfzo0difsn  10397  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemab  10491  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemstep  10503  remullem  10882  qdenre  11213  maxabslemval  11219  xrmaxiflemval  11260  summodclem2a  11391  fsum3  11397  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  sumsplitdc  11442  fsummulc2  11458  isumlessdc  11506  prodmodclem3  11585  prodmodclem2a  11586  prodmodclem2  11587  prodmodc  11588  fprodeq0  11627  sin02gt0  11773  p1modz1  11803  divconjdvds  11857  addmodlteqALT  11867  ltoddhalfle  11900  4dvdseven  11924  dfgcd2  12017  rppwr  12031  qredeq  12098  divgcdcoprmex  12104  cncongr1  12105  dvdsnprmd  12127  oddprmge3  12137  isprm5  12144  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem19  12284  difsqpwdvds  12339  oddprmdvds  12354  ennnfoneleminc  12414  ctinf  12433  ssomct  12448  sgrpidmndm  12826  idmhm  12865  mhmf1o  12866  insubm  12877  0mhm  12878  mhmco  12879  grpinvid1  12929  grpinvid2  12930  grplcan  12937  dfgrp3m  12974  dfgrp3me  12975  mhmfmhm  12986  issubg2m  13054  issubg4m  13058  srglmhm  13181  srgrmhm  13182  ringlz  13227  ringrz  13228  ringinvnzdiv  13232  ring1  13241  unitgrp  13290  subrgunit  13365  issubrg2  13367  islmodd  13388  upxp  13811  bdmopn  14043  suplociccex  14142  ptolemy  14284  dceqnconst  14846  dcapnconst  14847