Theorem jca 306

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
jca.1	|- ( ph -> ps )
jca.2	|- ( ph -> ch )

Assertion

Ref	Expression
jca	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 |- ( ph -> ps )
2		jca.2	. 2 |- ( ph -> ch )
3		pm3.2 139	. 2 |- ( ps -> ( ch -> ( ps /\ ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  jca31  309  jca32  310  jcai  311  jctil  312  jctir  313  ancli  323  ancri  324  sylanbrc  417  jcab  603  biadanid  614  ioran  754  ordi  818  stdcndc  847  stdcndcOLD  848  dfandc  886  mpbi2and  946  mpbir2and  947  pm4.82  953  pm4.83dc  954  rnlem  979  syl22anc  1251  syl112anc  1254  syl121anc  1255  syl211anc  1256  syl23anc  1257  syl32anc  1258  syl122anc  1259  syl212anc  1260  syl221anc  1261  syl222anc  1266  syl123anc  1267  syl132anc  1268  syl213anc  1269  syl231anc  1270  syl312anc  1271  syl321anc  1272  syl223anc  1276  syl232anc  1277  syl322anc  1278  syl233anc  1279  syl323anc  1280  syl332anc  1281  ecased  1362  19.26  1505  nfand  1592  19.40  1655  equsexd  1753  sbcof2  1834  sbequ8  1871  eu2  2100  eu3h  2101  eu5  2103  mooran2  2129  datisi  2166  felapton  2170  darapti  2171  dimatis  2173  fresison  2174  fesapo  2176  reximssdv  2612  r19.26  2634  r19.29af2  2648  r19.40  2662  eqvinc  2903  eqvincg  2904  elrabd  2938  reu6  2969  reu3  2970  indifdir  3437  undif3ss  3442  un00  3515  eqifdc  3616  disjpr2  3707  prel12  3825  prneimg  3828  preqsn  3829  disjiun  4054  opth  4299  0nelop  4310  euotd  4317  opelopabsb  4324  ispod  4369  elon2  4441  unexb  4507  opeluu  4515  eusvnfb  4519  suc11g  4623  nlimsucg  4632  tfi  4648  vtoclr  4741  opthprc  4744  ideqg  4847  resiexg  5023  dminss  5116  imainss  5117  ssxpbm  5137  relrelss  5228  funopg  5324  fununfun  5336  fntpg  5349  fun11uni  5363  imain  5375  funimaexglem  5376  funssxp  5465  ffdm  5466  f00  5489  dffo2  5524  fodmrnu  5528  foco  5531  fun11iun  5565  f1o00  5580  fsnd  5588  fv3  5622  dff2  5747  dff3im  5748  dffo4  5751  ffnfv  5761  ffvresb  5766  fsn2  5777  fconstfvm  5825  fnfvima  5842  fcof1o  5881  isocnv  5903  isotr  5908  riotaprop  5946  acexmidlemcase  5962  caovlem2d  6162  f1ocnvd  6171  caofcom  6212  resfunexgALT  6216  elxp7  6279  2ndrn  6292  1stconst  6330  2ndconst  6331  cnvf1olem  6333  poxp  6341  dftpos4  6372  dfsmo2  6396  tfrlem5  6423  tfrlemiex  6440  tfr1onlemsucaccv  6450  tfr1onlembfn  6453  tfr1onlemex  6456  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembfn  6466  tfrcllemex  6469  tfrcllemres  6471  tfrcl  6473  frecabex  6507  frecabcl  6508  frecfcllem  6513  frecrdg  6517  oawordi  6578  nntri3  6606  nntr2  6612  nnmordi  6625  iserd  6669  relelec  6685  erth  6689  qliftfun  6727  mapsncnv  6805  mptelixpg  6844  bren  6858  pw2f1odclem  6956  findcard2d  7014  findcard2sd  7015  isinfinf  7020  tridc  7022  nnwetri  7039  undifdcss  7046  fiintim  7054  fisseneq  7057  fidcenumlemim  7080  sbthlemi9  7093  supisolem  7136  ordiso2  7163  updjud  7210  difinfsn  7228  ctssdccl  7239  nnnninfeq  7256  omniwomnimkv  7295  pr2cv  7331  acfun  7350  exmidontriimlem2  7365  onntri45  7387  dftap2  7398  netap  7401  2omotaplemap  7404  ccfunen  7411  cc4f  7416  cc4n  7418  elni2  7462  dfplpq2  7502  dfmpq2  7503  enqbreq2  7505  enqdc1  7510  addcmpblnq  7515  addclnq  7523  nqpi  7526  addassnqg  7530  mulassnqg  7532  mulcanenq  7533  distrnqg  7535  1qec  7536  recexnq  7538  subhalfnqq  7562  enq0tr  7582  nqnq0pi  7586  nq0nn  7590  mulcanenq0ec  7593  nnnq0lem1  7594  addclnq0  7599  distrnq0  7607  addassnq0lemcl  7609  elnp1st2nd  7624  prarloc  7651  addlocprlemlt  7679  addlocprlemeq  7681  addlocprlemgt  7682  addclpr  7685  nqprm  7690  mullocprlem  7718  mullocpr  7719  mulclpr  7720  ltpopr  7743  ltaddpr  7745  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemrnd  7753  ltexprlemdisj  7754  addcanprleml  7762  addcanprlemu  7763  addcanprg  7764  recexprlemm  7772  recexprlemopl  7773  recexprlemopu  7775  recexprlemrnd  7777  recexprlemdisj  7778  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemopu  7796  cauappcvgprlemrnd  7798  cauappcvgprlemdisj  7799  cauappcvgprlemlim  7809  caucvgprlemnkj  7814  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemopu  7819  caucvgprlemrnd  7821  caucvgprlemlim  7829  caucvgprprlemnkltj  7837  caucvgprprlemnkeqj  7838  caucvgprprlemnjltk  7839  caucvgprprlemm  7844  caucvgprprlemopl  7845  caucvgprprlemopu  7847  caucvgprprlemrnd  7849  caucvgprprlemexbt  7854  caucvgprprlemlim  7859  suplocexprlemrl  7865  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemex  7870  suplocexprlemub  7871  prsrlem1  7890  mulclsr  7902  mulasssrg  7906  distrsrg  7907  suplocsrlemb  7954  elreal2  7978  axmulass  8021  axdistr  8022  axcaucvglemcau  8046  add20  8582  mullt0  8588  rereim  8694  ltmul1  8700  cru  8710  mulap0r  8723  aprcl  8754  aptap  8758  divmuldivap  8820  divmuleqap  8825  divadddivap  8835  divmuldivapd  8940  divmuleqapd  8941  div2subap  8945  ltmul12a  8968  lemul12a  8970  lemulge11  8974  lediv12a  9002  lediv2a  9003  recgt1i  9006  recreclt  9008  ledivp1  9011  lemul1ad  9047  lemul2ad  9048  ltmul12ad  9049  lemul12ad  9050  lemul12bd  9051  nndivre  9107  nndivtr  9113  halfaddsubcl  9305  halfaddsub  9306  lt2halves  9308  nnrecl  9328  elnn0nn  9372  elnnnn0b  9374  elnnnn0c  9375  nn0addge1  9376  nn0addge2  9377  xnn0xrnemnf  9405  elnn0z  9420  elnnz1  9430  nzadd  9460  elz2  9479  zdivadd  9497  zdivmul  9498  zextle  9499  peano2uz2  9515  uzind  9519  btwnz  9527  uzss  9704  eluzp1m1  9707  infregelbex  9754  eluz2b2  9759  qre  9781  qaddcl  9791  qmulcl  9793  qreccl  9798  irradd  9802  irrmul  9803  elpqb  9806  cnref1o  9807  rprege0  9825  rprene0  9828  rpreap0  9829  rpcnne0  9830  rpcnap0  9831  rpregt0d  9860  rprege0d  9861  rprene0d  9862  rpcnne0d  9863  lediv2ad  9876  ledivge1le  9883  lediv12ad  9913  nnledivrp  9923  nn0ledivnn  9924  xrlttri3  9954  xrrebnd  9976  xrrege0  9982  xnn0xadd0  10024  xlesubadd  10040  elioo4g  10091  ioomax  10105  iccmax  10106  divelunit  10159  elfz5  10174  uzsubsubfz  10204  fzopth  10218  fzass4  10219  fzrev2  10242  uzsplit  10249  elfz2nn0  10269  difelfzle  10291  1fv  10296  4fvwrd4  10297  fzo1fzo0n0  10344  elfzom1elp1fzo  10368  subfzo0  10408  infssuzex  10413  qtri3or  10420  adddivflid  10472  flltdivnn0lt  10484  intfracq  10502  modqid2  10533  modfzo0difsn  10577  seq3val  10642  seqvalcd  10643  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemmo  10687  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seqf1oglem1  10701  seqf1oglem2  10702  expclzaplem  10745  leexp1a  10776  expubnd  10778  le2sq2  10797  sumsqeq0  10800  bernneq  10842  expnlbnd  10846  nn0opthd  10904  faclbnd6  10926  facavg  10928  seq3coll  11024  hash2en  11025  wrdnval  11061  ccat0  11090  ccatsymb  11096  swrdspsleq  11158  pfxtrcfv  11184  pfxsuffeqwrdeq  11189  wrd2ind  11214  pfxccatin12lem2a  11218  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  pfxccatpfx1  11227  pfxccatpfx2  11228  swrdccatin1d  11234  swrdccatin2d  11235  shftlem  11242  shftfvalg  11244  shftfval  11247  cvg1nlemcau  11410  cvg1nlemres  11411  rexuz3  11416  resqrexlemcvg  11445  resqrexlemglsq  11448  resqrexlemga  11449  sqrtle  11462  sqrtlt  11463  sqrt11  11465  sqrtsq2  11469  absmul  11495  sqabs  11508  abslt  11514  absle  11515  lenegsq  11521  maxleastb  11640  maxltsup  11644  rexanre  11646  negfi  11654  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxltsup  11684  xrmaxadd  11687  climcn2  11735  mulcn2  11738  summodclem2a  11807  summodc  11809  fsum3  11813  fsum3cvg3  11822  fsumcl2lem  11824  fsumadd  11832  fsump1i  11859  fsum0diaglem  11866  mptfzshft  11868  fsumrev  11869  fsummulc2  11874  fsum00  11888  expcnvap0  11928  mertenslemi1  11961  ntrivcvgap0  11975  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodrev  12045  fprodconst  12046  eftlub  12116  efieq  12161  sincos1sgn  12191  demoivreALT  12200  dvdsval3  12217  dvdscmul  12244  dvdsmulc  12245  dvdscmulr  12246  dvdsmulcr  12247  modmulconst  12249  dvds2ln  12250  ltoddhalfle  12319  nn0o  12333  divalg2  12352  ndvdssub  12356  ndvdsadd  12357  divgcdz  12407  gcd0id  12415  gcdaddm  12420  bezoutlemstep  12433  bezoutlemmain  12434  dfgcd3  12446  dfgcd2  12450  lcmcllem  12504  dvdslcm  12506  lcmgcdlem  12514  lcmgcdnn  12519  qredeq  12533  qredeu  12534  rpdvds  12536  divgcdcoprm0  12538  cncongr1  12540  cncongr2  12541  cncongrcoprm  12543  prmind2  12557  isprm5  12579  isprm6  12584  prmexpb  12588  cncongrprm  12594  sqrt2irrlem  12598  pw2dvdslemn  12602  oddpwdclemxy  12606  oddpwdclemdc  12610  oddpwdc  12611  hashdvds  12658  prmdiv  12672  hashgcdlem  12675  nnoddn2prmb  12700  pythagtriplem6  12708  pythagtriplem7  12709  pcpre1  12730  pccl  12737  pcmul  12739  pcdiv  12740  pcqmul  12741  pcqcl  12744  pcdvds  12753  pcndvds  12755  pcndvds2  12757  pc2dvds  12768  dvdsprmpweqle  12775  difsqpwdvds  12776  pcaddlem  12777  pcadd  12778  pcmptcl  12780  pcmpt  12781  fldivp1  12786  pcfac  12788  oddprmdvds  12792  infpnlem2  12798  4sqlem5  12820  4sqlem6  12821  4sqlem4a  12829  4sqexercise1  12836  4sqexercise2  12837  4sqlem13m  12841  4sqlem15  12843  4sqlem16  12844  ennnfonelemfun  12903  ennnfonelemim  12910  ctinfomlemom  12913  ctinfom  12914  ctinf  12916  ctiunctlemfo  12925  omctfn  12929  fnpr2ob  13287  ismgmid2  13327  fngsum  13335  igsumvalx  13336  gsumfzval  13338  gsum0g  13343  gsumval2  13344  issgrpd  13359  ismndd  13384  prdsidlem  13394  imasmnd2  13399  mhmf1o  13417  subsubm  13430  dfgrp2  13474  isgrpid2  13487  isgrpinv  13501  grplrinv  13504  dfgrp3mlem  13545  dfgrp3m  13546  dfgrp3me  13547  prdsinvlem  13555  imasgrp2  13561  mhmmnd  13567  issubg2m  13640  issubgrpd2  13641  grpissubg  13645  subsubg  13648  subgintm  13649  isnsg3  13658  nmzsubg  13661  eqgval  13674  eqgen  13678  isghmd  13703  ghmrn  13708  ghmpreima  13717  ghmf1o  13726  conjghm  13727  conjnmzb  13731  ghmpropd  13734  rinvmod  13760  imasabl  13787  rnglz  13822  isrngd  13830  srgdilem  13846  srglmhm  13870  srgrmhm  13871  ringdilem  13889  isringd  13918  ringsrg  13924  ringinvnzdiv  13927  imasring  13941  dvdsrd  13971  unitgrp  13993  isrim0  14038  isrhm2d  14042  rhmf1o  14045  rhmco  14051  rhmopp  14053  issubrng2  14087  subsubrng  14091  subrgugrp  14117  issubrg2  14118  subsubrg  14122  resrhm  14125  aprap  14163  lmodfopnelem2  14202  lsssubg  14254  islss3  14256  islss4  14259  lspsnel6  14285  lidlacl  14361  lidlsubg  14363  lidlrsppropdg  14372  2idlelbas  14393  cnfld1  14449  cnsubglem  14456  mulgghm2  14485  zndvds  14526  mplsubgfi  14578  topgele  14616  tgcl  14651  epttop  14677  opnssneib  14743  iscnp4  14805  cnco  14808  cncnp  14817  cnrest2  14823  lmss  14833  txcnp  14858  txcn  14862  cnmpt12  14874  cnmpt22  14881  hmeof1o  14896  psmetres2  14920  distspace  14922  ismeti  14933  isxmetd  14934  xmetpsmet  14956  xblss2ps  14991  xblss2  14992  blcntrps  15002  blcntr  15003  blin2  15019  mopni3  15071  metequiv2  15083  bdmet  15089  xmettx  15097  cnbl0  15121  cnblcld  15122  tgioo  15141  elcncf1di  15166  dedekindeulemlu  15208  suplociccex  15212  dedekindicclemlu  15217  dedekindicc  15220  ivthinclemlopn  15223  ivthdec  15231  ivthreinc  15232  ivthdichlem  15238  cnplimcim  15254  limccnp2lem  15263  dvfvalap  15268  plymullem  15337  reeff1olem  15358  sin0pilem1  15368  pilem3  15370  ptolemy  15411  sincosq1sgn  15413  sinq12gt0  15417  ioocosf1o  15441  rprelogbmulexp  15543  perfectlem2  15587  lgslem3  15594  lgsne0  15630  gausslemma2dlem0b  15642  gausslemma2dlem0c  15643  lgsquadlem2  15670  lgsquad2lem2  15674  2lgsoddprmlem2  15698  2sqlem8  15715  gropd  15761  grstructd2dom  15762  incistruhgr  15801  umgrislfupgrenlem  15836  umgrislfupgrdom  15837  bj-nnan  15872  bj-charfun  15942  bdop  16010  bdunexb  16055  bj-om  16072  findset  16080  bj-peano4  16090  bj-inf2vn  16109  bj-inf2vn2  16110  pwle2  16137  pwf1oexmid  16138  nnnninfex  16161  sbthom  16167  qdencn  16168  trilpolemlt1  16182