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  1220  syl13anc  1222  syl31anc  1223  syl113anc  1232  syl131anc  1233  syl311anc  1234  syl33anc  1235  syl133anc  1243  syl313anc  1244  syl331anc  1245  syl333anc  1252  3jaob  1284  mp3and  1322  issod  4279  tfrlemibxssdm  6274  tfr1onlembxssdm  6290  tfrcllembxssdm  6303  ctssdccl  7055  onntri35  7172  ltexnqq  7328  enq0tr  7354  prarloc  7423  addclpr  7457  nqprxx  7466  mulclpr  7492  ltexprlempr  7528  recexprlempr  7552  cauappcvgprlemcl  7573  caucvgprlemcl  7596  caucvgprprlemcl  7624  suplocexprlemex  7642  le2tri3i  7985  ltmul1  8467  nn0ge2m1nn  9150  nn0ge0div  9251  eluzp1p1  9464  peano2uz  9494  zgt1rpn0n1  9602  ledivge1le  9633  elioc2  9840  elico2  9841  elicc2  9842  iccsupr  9870  uzsubsubfz  9949  fzrev3  9989  elfz1b  9992  fseq1p1m1  9996  elfz0ubfz0  10024  elfz0fzfz0  10025  fz0fzelfz0  10026  fz0fzdiffz0  10029  elfzmlbp  10031  elfzo2  10049  elfzo0  10081  fzo1fzo0n0  10082  elfzo0z  10083  fzofzim  10087  elfzo1  10089  ubmelfzo  10099  elfzodifsumelfzo  10100  elfzom1elp1fzo  10101  fzossfzop1  10111  ssfzo12bi  10124  subfzo0  10141  fldiv4p1lem1div2  10204  intqfrac2  10218  intfracq  10219  modfzo0difsn  10294  iseqf1olemqcl  10385  iseqf1olemnab  10387  iseqf1olemab  10388  seq3f1olemqsumkj  10397  seq3f1olemqsumk  10398  seq3f1olemstep  10400  remullem  10771  qdenre  11102  maxabslemval  11108  xrmaxiflemval  11147  summodclem2a  11278  fsum3  11284  fsum3cvg3  11293  fsumcl2lem  11295  fsumadd  11303  sumsplitdc  11329  fsummulc2  11345  isumlessdc  11393  prodmodclem3  11472  prodmodclem2a  11473  prodmodclem2  11474  prodmodc  11475  fprodeq0  11514  sin02gt0  11660  p1modz1  11690  divconjdvds  11741  addmodlteqALT  11751  ltoddhalfle  11784  4dvdseven  11808  dfgcd2  11898  rppwr  11912  qredeq  11973  divgcdcoprmex  11979  cncongr1  11980  dvdsnprmd  12002  oddprmge3  12012  ennnfoneleminc  12151  ctinf  12170  ssomct  12185  upxp  12683  bdmopn  12915  suplociccex  13014  ptolemy  13156  dceqnconst  13641  dcapnconst  13642