Theorem 3jca 1180

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3jcad  1181  mpbir3and  1183  syl3anbrc  1184  3anim123i  1187  syl3anc  1250  syl13anc  1252  syl31anc  1253  syl113anc  1262  syl131anc  1263  syl311anc  1264  syl33anc  1265  syl133anc  1273  syl313anc  1274  syl331anc  1275  syl333anc  1282  3jaob  1315  mp3and  1353  issod  4384  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  ctssdccl  7239  onntri35  7383  dftap2  7398  ltexnqq  7556  enq0tr  7582  prarloc  7651  addclpr  7685  nqprxx  7694  mulclpr  7720  ltexprlempr  7756  recexprlempr  7780  cauappcvgprlemcl  7801  caucvgprlemcl  7824  caucvgprprlemcl  7852  suplocexprlemex  7870  mpomulf  8097  le2tri3i  8216  ltmul1  8700  nn0ge2m1nn  9390  difgtsumgt  9477  nn0ge0div  9495  eluzp1p1  9709  peano2uz  9739  zgt1rpn0n1  9852  ledivge1le  9883  elioc2  10093  elico2  10094  elicc2  10095  iccsupr  10123  elfzd  10173  uzsubsubfz  10204  fzrev3  10244  elfz1b  10247  fseq1p1m1  10251  elfz0ubfz0  10282  elfz0fzfz0  10283  fz0fzelfz0  10284  fz0fzdiffz0  10287  elfzmlbp  10289  elfzo2  10307  elfzo0  10343  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  elfzo1  10351  ubmelfzo  10366  elfzodifsumelfzo  10367  elfzom1elp1fzo  10368  fzossfzop1  10378  ssfzo12bi  10391  subfzo0  10408  fldiv4p1lem1div2  10485  intqfrac2  10501  intfracq  10502  modfzo0difsn  10577  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemstep  10696  seqf1oglem2  10702  wrdlenge2n0  11066  ccatval21sw  11099  ccatass  11102  lswccatn0lsw  11105  wrdl1s1  11122  swrdlen2  11153  swrdfv2  11154  swrdspsleq  11158  swrdccat2  11162  pfxnd  11180  swrdswrdlem  11195  swrdpfx  11198  pfxpfx  11199  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2c  11221  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  remullem  11297  qdenre  11628  maxabslemval  11634  xrmaxiflemval  11676  summodclem2a  11807  fsum3  11813  fsum3cvg3  11822  fsumcl2lem  11824  fsumadd  11832  sumsplitdc  11858  fsummulc2  11874  isumlessdc  11922  prodmodclem3  12001  prodmodclem2a  12002  prodmodclem2  12003  prodmodc  12004  fprodeq0  12043  sin02gt0  12190  p1modz1  12220  divconjdvds  12275  addmodlteqALT  12285  ltoddhalfle  12319  4dvdseven  12343  dfgcd2  12450  rppwr  12464  qredeq  12533  divgcdcoprmex  12539  cncongr1  12540  dvdsnprmd  12562  oddprmge3  12572  isprm5  12579  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem19  12720  difsqpwdvds  12776  oddprmdvds  12792  ennnfoneleminc  12897  ctinf  12916  ssomct  12931  sgrpidmndm  13367  idmhm  13416  mhmf1o  13417  insubm  13432  0mhm  13433  resmhm  13434  resmhm2  13435  resmhm2b  13436  mhmco  13437  grpinvid1  13499  grpinvid2  13500  grplcan  13509  dfgrp3m  13546  dfgrp3me  13547  mhmfmhm  13568  issubg2m  13640  issubg4m  13644  ghmmhm  13704  rngrz  13823  srglmhm  13870  srgrmhm  13871  ringlz  13920  ringrz  13921  ringinvnzdiv  13927  ring1  13936  unitgrp  13993  isrhm2d  14042  subrgunit  14116  issubrg2  14118  islmodd  14170  dflidl2rng  14358  rnglidlmmgm  14373  quscrng  14410  upxp  14859  bdmopn  15091  suplociccex  15212  ivthreinc  15232  ptolemy  15411  perfectlem1  15586  gausslemma2dlem1a  15650  gausslemma2dlem4  15656  dceqnconst  16201  dcapnconst  16202