Theorem 3jca 1172

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 307	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		df-3an 975	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 133	1 |- ( ph -> ( ps /\ ch /\ th ) )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3jcad  1173  mpbir3and  1175  syl3anbrc  1176  3anim123i  1179  syl3anc  1233  syl13anc  1235  syl31anc  1236  syl113anc  1245  syl131anc  1246  syl311anc  1247  syl33anc  1248  syl133anc  1256  syl313anc  1257  syl331anc  1258  syl333anc  1265  3jaob  1297  mp3and  1335  issod  4304  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  ctssdccl  7088  onntri35  7214  ltexnqq  7370  enq0tr  7396  prarloc  7465  addclpr  7499  nqprxx  7508  mulclpr  7534  ltexprlempr  7570  recexprlempr  7594  cauappcvgprlemcl  7615  caucvgprlemcl  7638  caucvgprprlemcl  7666  suplocexprlemex  7684  le2tri3i  8028  ltmul1  8511  nn0ge2m1nn  9195  difgtsumgt  9281  nn0ge0div  9299  eluzp1p1  9512  peano2uz  9542  zgt1rpn0n1  9652  ledivge1le  9683  elioc2  9893  elico2  9894  elicc2  9895  iccsupr  9923  uzsubsubfz  10003  fzrev3  10043  elfz1b  10046  fseq1p1m1  10050  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzmlbp  10088  elfzo2  10106  elfzo0  10138  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzo1  10146  ubmelfzo  10156  elfzodifsumelfzo  10157  elfzom1elp1fzo  10158  fzossfzop1  10168  ssfzo12bi  10181  subfzo0  10198  fldiv4p1lem1div2  10261  intqfrac2  10275  intfracq  10276  modfzo0difsn  10351  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemstep  10457  remullem  10835  qdenre  11166  maxabslemval  11172  xrmaxiflemval  11213  summodclem2a  11344  fsum3  11350  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  sumsplitdc  11395  fsummulc2  11411  isumlessdc  11459  prodmodclem3  11538  prodmodclem2a  11539  prodmodclem2  11540  prodmodc  11541  fprodeq0  11580  sin02gt0  11726  p1modz1  11756  divconjdvds  11809  addmodlteqALT  11819  ltoddhalfle  11852  4dvdseven  11876  dfgcd2  11969  rppwr  11983  qredeq  12050  divgcdcoprmex  12056  cncongr1  12057  dvdsnprmd  12079  oddprmge3  12089  isprm5  12096  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem19  12236  difsqpwdvds  12291  oddprmdvds  12306  ennnfoneleminc  12366  ctinf  12385  ssomct  12400  sgrpidmndm  12656  idmhm  12692  mhmf1o  12693  insubm  12703  0mhm  12704  mhmco  12705  grpinvid1  12754  grpinvid2  12755  grplcan  12761  upxp  13066  bdmopn  13298  suplociccex  13397  ptolemy  13539  dceqnconst  14091  dcapnconst  14092