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	⊢ (𝜑 → 𝜓)
jca.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
jca	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca.2	. 2 ⊢ (𝜑 → 𝜒)
3		pm3.2 139	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒)))
4	1, 2, 3	sylc 62	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

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  753  ordi  817  stdcndc  846  stdcndcOLD  847  dfandc  885  mpbi2and  945  mpbir2and  946  pm4.82  952  pm4.83dc  953  rnlem  978  syl22anc  1250  syl112anc  1253  syl121anc  1254  syl211anc  1255  syl23anc  1256  syl32anc  1257  syl122anc  1258  syl212anc  1259  syl221anc  1260  syl222anc  1265  syl123anc  1266  syl132anc  1267  syl213anc  1268  syl231anc  1269  syl312anc  1270  syl321anc  1271  syl223anc  1275  syl232anc  1276  syl322anc  1277  syl233anc  1278  syl323anc  1279  syl332anc  1280  ecased  1361  19.26  1503  nfand  1590  19.40  1653  equsexd  1751  sbcof2  1832  sbequ8  1869  eu2  2097  eu3h  2098  eu5  2100  mooran2  2126  datisi  2163  felapton  2167  darapti  2168  dimatis  2170  fresison  2171  fesapo  2173  reximssdv  2609  r19.26  2631  r19.29af2  2645  r19.40  2659  eqvinc  2895  eqvincg  2896  elrabd  2930  reu6  2961  reu3  2962  indifdir  3428  undif3ss  3433  un00  3506  eqifdc  3606  disjpr2  3696  prel12  3811  prneimg  3814  preqsn  3815  disjiun  4038  opth  4280  0nelop  4291  euotd  4298  opelopabsb  4305  ispod  4350  elon2  4422  unexb  4488  opeluu  4496  eusvnfb  4500  suc11g  4604  nlimsucg  4613  tfi  4629  vtoclr  4722  opthprc  4725  ideqg  4828  resiexg  5003  dminss  5096  imainss  5097  ssxpbm  5117  relrelss  5208  funopg  5304  fununfun  5316  fntpg  5329  fun11uni  5343  imain  5355  funimaexglem  5356  funssxp  5444  ffdm  5445  f00  5466  dffo2  5501  fodmrnu  5505  foco  5508  fun11iun  5542  f1o00  5556  fsnd  5564  fv3  5598  dff2  5723  dff3im  5724  dffo4  5727  ffnfv  5737  ffvresb  5742  fsn2  5753  fconstfvm  5801  fnfvima  5818  fcof1o  5857  isocnv  5879  isotr  5884  riotaprop  5922  acexmidlemcase  5938  caovlem2d  6138  f1ocnvd  6147  caofcom  6188  resfunexgALT  6192  elxp7  6255  2ndrn  6268  1stconst  6306  2ndconst  6307  cnvf1olem  6309  poxp  6317  dftpos4  6348  dfsmo2  6372  tfrlem5  6399  tfrlemiex  6416  tfr1onlemsucaccv  6426  tfr1onlembfn  6429  tfr1onlemex  6432  tfr1onlemres  6434  tfrcllemsucaccv  6439  tfrcllembfn  6442  tfrcllemex  6445  tfrcllemres  6447  tfrcl  6449  frecabex  6483  frecabcl  6484  frecfcllem  6489  frecrdg  6493  oawordi  6554  nntri3  6582  nntr2  6588  nnmordi  6601  iserd  6645  relelec  6661  erth  6665  qliftfun  6703  mapsncnv  6781  mptelixpg  6820  bren  6834  pw2f1odclem  6930  findcard2d  6987  findcard2sd  6988  isinfinf  6993  tridc  6995  nnwetri  7012  undifdcss  7019  fiintim  7027  fisseneq  7030  fidcenumlemim  7053  sbthlemi9  7066  supisolem  7109  ordiso2  7136  updjud  7183  difinfsn  7201  ctssdccl  7212  nnnninfeq  7229  omniwomnimkv  7268  acfun  7318  exmidontriimlem2  7333  onntri45  7352  dftap2  7362  netap  7365  2omotaplemap  7368  ccfunen  7375  cc4f  7380  cc4n  7382  elni2  7426  dfplpq2  7466  dfmpq2  7467  enqbreq2  7469  enqdc1  7474  addcmpblnq  7479  addclnq  7487  nqpi  7490  addassnqg  7494  mulassnqg  7496  mulcanenq  7497  distrnqg  7499  1qec  7500  recexnq  7502  subhalfnqq  7526  enq0tr  7546  nqnq0pi  7550  nq0nn  7554  mulcanenq0ec  7557  nnnq0lem1  7558  addclnq0  7563  distrnq0  7571  addassnq0lemcl  7573  elnp1st2nd  7588  prarloc  7615  addlocprlemlt  7643  addlocprlemeq  7645  addlocprlemgt  7646  addclpr  7649  nqprm  7654  mullocprlem  7682  mullocpr  7683  mulclpr  7684  ltpopr  7707  ltaddpr  7709  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemrnd  7717  ltexprlemdisj  7718  addcanprleml  7726  addcanprlemu  7727  addcanprg  7728  recexprlemm  7736  recexprlemopl  7737  recexprlemopu  7739  recexprlemrnd  7741  recexprlemdisj  7742  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemopu  7760  cauappcvgprlemrnd  7762  cauappcvgprlemdisj  7763  cauappcvgprlemlim  7773  caucvgprlemnkj  7778  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemopu  7783  caucvgprlemrnd  7785  caucvgprlemlim  7793  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnjltk  7803  caucvgprprlemm  7808  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemrnd  7813  caucvgprprlemexbt  7818  caucvgprprlemlim  7823  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemex  7834  suplocexprlemub  7835  prsrlem1  7854  mulclsr  7866  mulasssrg  7870  distrsrg  7871  suplocsrlemb  7918  elreal2  7942  axmulass  7985  axdistr  7986  axcaucvglemcau  8010  add20  8546  mullt0  8552  rereim  8658  ltmul1  8664  cru  8674  mulap0r  8687  aprcl  8718  aptap  8722  divmuldivap  8784  divmuleqap  8789  divadddivap  8799  divmuldivapd  8904  divmuleqapd  8905  div2subap  8909  ltmul12a  8932  lemul12a  8934  lemulge11  8938  lediv12a  8966  lediv2a  8967  recgt1i  8970  recreclt  8972  ledivp1  8975  lemul1ad  9011  lemul2ad  9012  ltmul12ad  9013  lemul12ad  9014  lemul12bd  9015  nndivre  9071  nndivtr  9077  halfaddsubcl  9269  halfaddsub  9270  lt2halves  9272  nnrecl  9292  elnn0nn  9336  elnnnn0b  9338  elnnnn0c  9339  nn0addge1  9340  nn0addge2  9341  xnn0xrnemnf  9369  elnn0z  9384  elnnz1  9394  nzadd  9424  elz2  9443  zdivadd  9461  zdivmul  9462  zextle  9463  peano2uz2  9479  uzind  9483  btwnz  9491  uzss  9668  eluzp1m1  9671  infregelbex  9718  eluz2b2  9723  qre  9745  qaddcl  9755  qmulcl  9757  qreccl  9762  irradd  9766  irrmul  9767  elpqb  9770  cnref1o  9771  rprege0  9789  rprene0  9792  rpreap0  9793  rpcnne0  9794  rpcnap0  9795  rpregt0d  9824  rprege0d  9825  rprene0d  9826  rpcnne0d  9827  lediv2ad  9840  ledivge1le  9847  lediv12ad  9877  nnledivrp  9887  nn0ledivnn  9888  xrlttri3  9918  xrrebnd  9940  xrrege0  9946  xnn0xadd0  9988  xlesubadd  10004  elioo4g  10055  ioomax  10069  iccmax  10070  divelunit  10123  elfz5  10138  uzsubsubfz  10168  fzopth  10182  fzass4  10183  fzrev2  10206  uzsplit  10213  elfz2nn0  10233  difelfzle  10255  1fv  10260  4fvwrd4  10261  fzo1fzo0n0  10305  elfzom1elp1fzo  10329  subfzo0  10369  infssuzex  10374  qtri3or  10381  adddivflid  10433  flltdivnn0lt  10445  intfracq  10463  modqid2  10494  modfzo0difsn  10538  seq3val  10603  seqvalcd  10604  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemmo  10648  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seqf1oglem1  10662  seqf1oglem2  10663  expclzaplem  10706  leexp1a  10737  expubnd  10739  le2sq2  10758  sumsqeq0  10761  bernneq  10803  expnlbnd  10807  nn0opthd  10865  faclbnd6  10887  facavg  10889  seq3coll  10985  hash2en  10986  wrdnval  11022  ccat0  11050  ccatsymb  11056  shftlem  11098  shftfvalg  11100  shftfval  11103  cvg1nlemcau  11266  cvg1nlemres  11267  rexuz3  11272  resqrexlemcvg  11301  resqrexlemglsq  11304  resqrexlemga  11305  sqrtle  11318  sqrtlt  11319  sqrt11  11321  sqrtsq2  11325  absmul  11351  sqabs  11364  abslt  11370  absle  11371  lenegsq  11377  maxleastb  11496  maxltsup  11500  rexanre  11502  negfi  11510  xrmaxiflemab  11529  xrmaxiflemlub  11530  xrmaxltsup  11540  xrmaxadd  11543  climcn2  11591  mulcn2  11594  summodclem2a  11663  summodc  11665  fsum3  11669  fsum3cvg3  11678  fsumcl2lem  11680  fsumadd  11688  fsump1i  11715  fsum0diaglem  11722  mptfzshft  11724  fsumrev  11725  fsummulc2  11730  fsum00  11744  expcnvap0  11784  mertenslemi1  11817  ntrivcvgap0  11831  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodrev  11901  fprodconst  11902  eftlub  11972  efieq  12017  sincos1sgn  12047  demoivreALT  12056  dvdsval3  12073  dvdscmul  12100  dvdsmulc  12101  dvdscmulr  12102  dvdsmulcr  12103  modmulconst  12105  dvds2ln  12106  ltoddhalfle  12175  nn0o  12189  divalg2  12208  ndvdssub  12212  ndvdsadd  12213  divgcdz  12263  gcd0id  12271  gcdaddm  12276  bezoutlemstep  12289  bezoutlemmain  12290  dfgcd3  12302  dfgcd2  12306  lcmcllem  12360  dvdslcm  12362  lcmgcdlem  12370  lcmgcdnn  12375  qredeq  12389  qredeu  12390  rpdvds  12392  divgcdcoprm0  12394  cncongr1  12396  cncongr2  12397  cncongrcoprm  12399  prmind2  12413  isprm5  12435  isprm6  12440  prmexpb  12444  cncongrprm  12450  sqrt2irrlem  12454  pw2dvdslemn  12458  oddpwdclemxy  12462  oddpwdclemdc  12466  oddpwdc  12467  hashdvds  12514  prmdiv  12528  hashgcdlem  12531  nnoddn2prmb  12556  pythagtriplem6  12564  pythagtriplem7  12565  pcpre1  12586  pccl  12593  pcmul  12595  pcdiv  12596  pcqmul  12597  pcqcl  12600  pcdvds  12609  pcndvds  12611  pcndvds2  12613  pc2dvds  12624  dvdsprmpweqle  12631  difsqpwdvds  12632  pcaddlem  12633  pcadd  12634  pcmptcl  12636  pcmpt  12637  fldivp1  12642  pcfac  12644  oddprmdvds  12648  infpnlem2  12654  4sqlem5  12676  4sqlem6  12677  4sqlem4a  12685  4sqexercise1  12692  4sqexercise2  12693  4sqlem13m  12697  4sqlem15  12699  4sqlem16  12700  ennnfonelemfun  12759  ennnfonelemim  12766  ctinfomlemom  12769  ctinfom  12770  ctinf  12772  ctiunctlemfo  12781  omctfn  12785  fnpr2ob  13143  ismgmid2  13183  fngsum  13191  igsumvalx  13192  gsumfzval  13194  gsum0g  13199  gsumval2  13200  issgrpd  13215  ismndd  13240  prdsidlem  13250  imasmnd2  13255  mhmf1o  13273  subsubm  13286  dfgrp2  13330  isgrpid2  13343  isgrpinv  13357  grplrinv  13360  dfgrp3mlem  13401  dfgrp3m  13402  dfgrp3me  13403  prdsinvlem  13411  imasgrp2  13417  mhmmnd  13423  issubg2m  13496  issubgrpd2  13497  grpissubg  13501  subsubg  13504  subgintm  13505  isnsg3  13514  nmzsubg  13517  eqgval  13530  eqgen  13534  isghmd  13559  ghmrn  13564  ghmpreima  13573  ghmf1o  13582  conjghm  13583  conjnmzb  13587  ghmpropd  13590  rinvmod  13616  imasabl  13643  rnglz  13678  isrngd  13686  srgdilem  13702  srglmhm  13726  srgrmhm  13727  ringdilem  13745  isringd  13774  ringsrg  13780  ringinvnzdiv  13783  imasring  13797  dvdsrd  13827  unitgrp  13849  isrim0  13894  isrhm2d  13898  rhmf1o  13901  rhmco  13907  rhmopp  13909  issubrng2  13943  subsubrng  13947  subrgugrp  13973  issubrg2  13974  subsubrg  13978  resrhm  13981  aprap  14019  lmodfopnelem2  14058  lsssubg  14110  islss3  14112  islss4  14115  lspsnel6  14141  lidlacl  14217  lidlsubg  14219  lidlrsppropdg  14228  2idlelbas  14249  cnfld1  14305  cnsubglem  14312  mulgghm2  14341  zndvds  14382  mplsubgfi  14434  topgele  14472  tgcl  14507  epttop  14533  opnssneib  14599  iscnp4  14661  cnco  14664  cncnp  14673  cnrest2  14679  lmss  14689  txcnp  14714  txcn  14718  cnmpt12  14730  cnmpt22  14737  hmeof1o  14752  psmetres2  14776  distspace  14778  ismeti  14789  isxmetd  14790  xmetpsmet  14812  xblss2ps  14847  xblss2  14848  blcntrps  14858  blcntr  14859  blin2  14875  mopni3  14927  metequiv2  14939  bdmet  14945  xmettx  14953  cnbl0  14977  cnblcld  14978  tgioo  14997  elcncf1di  15022  dedekindeulemlu  15064  suplociccex  15068  dedekindicclemlu  15073  dedekindicc  15076  ivthinclemlopn  15079  ivthdec  15087  ivthreinc  15088  ivthdichlem  15094  cnplimcim  15110  limccnp2lem  15119  dvfvalap  15124  plymullem  15193  reeff1olem  15214  sin0pilem1  15224  pilem3  15226  ptolemy  15267  sincosq1sgn  15269  sinq12gt0  15273  ioocosf1o  15297  rprelogbmulexp  15399  perfectlem2  15443  lgslem3  15450  lgsne0  15486  gausslemma2dlem0b  15498  gausslemma2dlem0c  15499  lgsquadlem2  15526  lgsquad2lem2  15530  2lgsoddprmlem2  15554  2sqlem8  15571  gropd  15615  grstructd2dom  15616  bj-nnan  15634  bj-charfun  15705  bdop  15773  bdunexb  15818  bj-om  15835  findset  15843  bj-peano4  15853  bj-inf2vn  15872  bj-inf2vn2  15873  pwle2  15897  pwf1oexmid  15898  nnnninfex  15921  sbthom  15927  qdencn  15928  trilpolemlt1  15942