Theorem 3jca 1161

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

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

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 964

This theorem is referenced by:  3jcad  1162  mpbir3and  1164  syl3anbrc  1165  3anim123i  1166  syl3anc  1216  syl13anc  1218  syl31anc  1219  syl113anc  1228  syl131anc  1229  syl311anc  1230  syl33anc  1231  syl133anc  1239  syl313anc  1240  syl331anc  1241  syl333anc  1248  3jaob  1280  mp3and  1318  issod  4241  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  ctssdccl  6996  ltexnqq  7216  enq0tr  7242  prarloc  7311  addclpr  7345  nqprxx  7354  mulclpr  7380  ltexprlempr  7416  recexprlempr  7440  cauappcvgprlemcl  7461  caucvgprlemcl  7484  caucvgprprlemcl  7512  suplocexprlemex  7530  le2tri3i  7872  ltmul1  8354  nn0ge2m1nn  9037  nn0ge0div  9138  eluzp1p1  9351  peano2uz  9378  ledivge1le  9513  elioc2  9719  elico2  9720  elicc2  9721  iccsupr  9749  uzsubsubfz  9827  fzrev3  9867  elfz1b  9870  fseq1p1m1  9874  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  elfzmlbp  9909  elfzo2  9927  elfzo0  9959  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  elfzo1  9967  ubmelfzo  9977  elfzodifsumelfzo  9978  elfzom1elp1fzo  9979  fzossfzop1  9989  ssfzo12bi  10002  subfzo0  10019  fldiv4p1lem1div2  10078  intqfrac2  10092  intfracq  10093  modfzo0difsn  10168  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemstep  10274  remullem  10643  qdenre  10974  maxabslemval  10980  xrmaxiflemval  11019  summodclem2a  11150  fsum3  11156  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  sumsplitdc  11201  fsummulc2  11217  isumlessdc  11265  prodmodclem3  11344  prodmodclem2a  11345  prodmodclem2  11346  prodmodc  11347  sin02gt0  11470  divconjdvds  11547  addmodlteqALT  11557  ltoddhalfle  11590  4dvdseven  11614  dfgcd2  11702  rppwr  11716  qredeq  11777  divgcdcoprmex  11783  cncongr1  11784  dvdsnprmd  11806  oddprmge3  11815  ennnfoneleminc  11924  ctinf  11943  upxp  12441  bdmopn  12673  suplociccex  12772  ptolemy  12905