Theorem 3jca 1162

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

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

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 965

This theorem is referenced by:  3jcad  1163  mpbir3and  1165  syl3anbrc  1166  3anim123i  1167  syl3anc  1217  syl13anc  1219  syl31anc  1220  syl113anc  1229  syl131anc  1230  syl311anc  1231  syl33anc  1232  syl133anc  1240  syl313anc  1241  syl331anc  1242  syl333anc  1249  3jaob  1281  mp3and  1319  issod  4249  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  ctssdccl  7004  ltexnqq  7240  enq0tr  7266  prarloc  7335  addclpr  7369  nqprxx  7378  mulclpr  7404  ltexprlempr  7440  recexprlempr  7464  cauappcvgprlemcl  7485  caucvgprlemcl  7508  caucvgprprlemcl  7536  suplocexprlemex  7554  le2tri3i  7896  ltmul1  8378  nn0ge2m1nn  9061  nn0ge0div  9162  eluzp1p1  9375  peano2uz  9405  zgt1rpn0n1  9512  ledivge1le  9543  elioc2  9749  elico2  9750  elicc2  9751  iccsupr  9779  uzsubsubfz  9858  fzrev3  9898  elfz1b  9901  fseq1p1m1  9905  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  fz0fzdiffz0  9938  elfzmlbp  9940  elfzo2  9958  elfzo0  9990  fzo1fzo0n0  9991  elfzo0z  9992  fzofzim  9996  elfzo1  9998  ubmelfzo  10008  elfzodifsumelfzo  10009  elfzom1elp1fzo  10010  fzossfzop1  10020  ssfzo12bi  10033  subfzo0  10050  fldiv4p1lem1div2  10109  intqfrac2  10123  intfracq  10124  modfzo0difsn  10199  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemstep  10305  remullem  10675  qdenre  11006  maxabslemval  11012  xrmaxiflemval  11051  summodclem2a  11182  fsum3  11188  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  sumsplitdc  11233  fsummulc2  11249  isumlessdc  11297  prodmodclem3  11376  prodmodclem2a  11377  prodmodclem2  11378  prodmodc  11379  sin02gt0  11506  divconjdvds  11583  addmodlteqALT  11593  ltoddhalfle  11626  4dvdseven  11650  dfgcd2  11738  rppwr  11752  qredeq  11813  divgcdcoprmex  11819  cncongr1  11820  dvdsnprmd  11842  oddprmge3  11851  ennnfoneleminc  11960  ctinf  11979  upxp  12480  bdmopn  12712  suplociccex  12811  ptolemy  12953  dceqnconst  13423