Theorem 3jca 1167

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

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

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 970

This theorem is referenced by:  3jcad  1168  mpbir3and  1170  syl3anbrc  1171  3anim123i  1174  syl3anc  1228  syl13anc  1230  syl31anc  1231  syl113anc  1240  syl131anc  1241  syl311anc  1242  syl33anc  1243  syl133anc  1251  syl313anc  1252  syl331anc  1253  syl333anc  1260  3jaob  1292  mp3and  1330  issod  4296  tfrlemibxssdm  6291  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  ctssdccl  7072  onntri35  7189  ltexnqq  7345  enq0tr  7371  prarloc  7440  addclpr  7474  nqprxx  7483  mulclpr  7509  ltexprlempr  7545  recexprlempr  7569  cauappcvgprlemcl  7590  caucvgprlemcl  7613  caucvgprprlemcl  7641  suplocexprlemex  7659  le2tri3i  8003  ltmul1  8486  nn0ge2m1nn  9170  difgtsumgt  9256  nn0ge0div  9274  eluzp1p1  9487  peano2uz  9517  zgt1rpn0n1  9627  ledivge1le  9658  elioc2  9868  elico2  9869  elicc2  9870  iccsupr  9898  uzsubsubfz  9978  fzrev3  10018  elfz1b  10021  fseq1p1m1  10025  elfz0ubfz0  10056  elfz0fzfz0  10057  fz0fzelfz0  10058  fz0fzdiffz0  10061  elfzmlbp  10063  elfzo2  10081  elfzo0  10113  fzo1fzo0n0  10114  elfzo0z  10115  fzofzim  10119  elfzo1  10121  ubmelfzo  10131  elfzodifsumelfzo  10132  elfzom1elp1fzo  10133  fzossfzop1  10143  ssfzo12bi  10156  subfzo0  10173  fldiv4p1lem1div2  10236  intqfrac2  10250  intfracq  10251  modfzo0difsn  10326  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemab  10420  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemstep  10432  remullem  10809  qdenre  11140  maxabslemval  11146  xrmaxiflemval  11187  summodclem2a  11318  fsum3  11324  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  sumsplitdc  11369  fsummulc2  11385  isumlessdc  11433  prodmodclem3  11512  prodmodclem2a  11513  prodmodclem2  11514  prodmodc  11515  fprodeq0  11554  sin02gt0  11700  p1modz1  11730  divconjdvds  11783  addmodlteqALT  11793  ltoddhalfle  11826  4dvdseven  11850  dfgcd2  11943  rppwr  11957  qredeq  12024  divgcdcoprmex  12030  cncongr1  12031  dvdsnprmd  12053  oddprmge3  12063  isprm5  12070  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem19  12210  difsqpwdvds  12265  oddprmdvds  12280  ennnfoneleminc  12340  ctinf  12359  ssomct  12374  upxp  12872  bdmopn  13104  suplociccex  13203  ptolemy  13345  dceqnconst  13898  dcapnconst  13899