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 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca31  309  jca32  310  jcai  311  jctil  312  jctir  313  ancli  323  ancri  324  sylanbrc  421  jcab  611  biadanid  622  ioran  764  ordi  828  stdcndc  857  stdcndcOLD  858  dfandc  896  mpbi2and  956  mpbir2and  957  pm4.82  963  pm4.83dc  964  rnlem  989  ifp2  993  syl22anc  1279  syl112anc  1282  syl121anc  1283  syl211anc  1284  syl23anc  1285  syl32anc  1286  syl122anc  1287  syl212anc  1288  syl221anc  1289  syl222anc  1294  syl123anc  1295  syl132anc  1296  syl213anc  1297  syl231anc  1298  syl312anc  1299  syl321anc  1300  syl223anc  1304  syl232anc  1305  syl322anc  1306  syl233anc  1307  syl323anc  1308  syl332anc  1309  ecased  1390  19.26  1534  nfand  1621  19.40  1684  equsexd  1782  sbcof2  1863  sbequ8  1900  eu2  2131  eu3h  2132  eu5  2134  mooran2  2160  datisi  2197  felapton  2201  darapti  2202  dimatis  2204  fresison  2205  fesapo  2207  reximssdv  2654  r19.26  2677  r19.29af2  2691  r19.40  2705  eqvinc  2949  eqvincg  2950  elrabd  2984  reu6  3015  reu3  3016  indifdir  3487  undif3ss  3492  un00  3567  vvin  3569  eqifdc  3677  disjpr2  3773  prel12  3896  prneimg  3899  preqsn  3900  disjiun  4125  opth  4377  0nelop  4388  euotd  4395  opelopabsb  4402  ispod  4449  elon2  4521  unexb  4588  opeluu  4596  eusvnfb  4600  suc11g  4704  nlimsucg  4713  tfi  4729  vtoclr  4823  opthprc  4826  ideqg  4931  resiexg  5108  dminss  5202  imainss  5203  ssxpbm  5223  relrelss  5314  funopg  5411  fununfun  5424  fntpg  5437  fun11uni  5451  imain  5463  funimaexglem  5464  funssxp  5557  ffdm  5558  f00  5584  dffo2  5619  fodmrnu  5623  foco  5626  fun11iun  5660  f1o00  5676  fsnd  5684  fv3  5718  fvun1d  5771  fvun2d  5772  dff2  5852  dff3im  5853  dffo4  5856  ffnfv  5866  ffvresb  5871  fsn2  5882  fconstfvm  5933  fnfvima  5953  resfvresima  5956  fcof1o  5995  isocnv  6017  isotr  6022  riotaprop  6064  acexmidlemcase  6080  caovlem2d  6282  f1ocnvd  6292  f1o3d  6298  caofcom  6333  resfunexgALT  6337  elxp7  6404  2ndrn  6417  1stconst  6457  2ndconst  6458  cnvf1olem  6460  poxp  6468  ressuppss  6494  funsssuppss  6498  dftpos4  6534  dfsmo2  6558  tfrlem5  6585  tfrlemiex  6602  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemex  6618  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemex  6631  tfrcllemres  6633  tfrcl  6635  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecrdg  6679  oawordi  6742  nntri3  6770  nntr2  6776  nnmordi  6789  iserd  6833  relelec  6849  erth  6853  qliftfun  6891  mapsnd  6970  mapsncnv  6977  mptelixpg  7016  bren  7030  pw2f1odclem  7134  mapunen  7151  findcard2d  7195  findcard2sd  7196  isinfinf  7201  tridc  7204  nnwetri  7223  undifdcss  7230  fiintim  7238  fisseneq  7242  fidcenumlemim  7269  sbthlemi9  7282  supisolem  7348  ordiso2  7375  updjud  7422  difinfsn  7440  ctssdccl  7451  nnnninfeq  7468  omniwomnimkv  7507  pr2cv  7543  acfun  7563  exmidontriimlem2  7578  onntri45  7600  dftap2  7617  netap  7620  2omotaplemap  7623  ccfunen  7630  cc4f  7635  cc4n  7637  elni2  7681  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enqdc1  7729  addcmpblnq  7734  addclnq  7742  nqpi  7745  addassnqg  7749  mulassnqg  7751  mulcanenq  7752  distrnqg  7754  1qec  7755  recexnq  7757  subhalfnqq  7781  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  mulcanenq0ec  7812  nnnq0lem1  7813  addclnq0  7818  distrnq0  7826  addassnq0lemcl  7828  elnp1st2nd  7843  prarloc  7870  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  addclpr  7904  nqprm  7909  mullocprlem  7937  mullocpr  7938  mulclpr  7939  ltpopr  7962  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemrnd  7972  ltexprlemdisj  7973  addcanprleml  7981  addcanprlemu  7982  addcanprg  7983  recexprlemm  7991  recexprlemopl  7992  recexprlemopu  7994  recexprlemrnd  7996  recexprlemdisj  7997  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemrnd  8017  cauappcvgprlemdisj  8018  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemrnd  8040  caucvgprlemlim  8048  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemm  8063  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemrnd  8068  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  prsrlem1  8109  mulclsr  8121  mulasssrg  8125  distrsrg  8126  suplocsrlemb  8173  elreal2  8197  axmulass  8240  axdistr  8241  axcaucvglemcau  8265  add20  8802  mullt0  8808  rereim  8914  ltmul1  8920  cru  8930  mulap0r  8943  aprcl  8974  aptap  8978  divmuldivap  9042  divmuleqap  9047  divadddivap  9057  divmuldivapd  9162  divmuleqapd  9163  div2subap  9167  ltmul12a  9190  lemul12a  9192  lemulge11  9196  lediv12a  9224  lediv2a  9225  recgt1i  9228  recreclt  9230  ledivp1  9233  lemul1ad  9269  lemul2ad  9270  ltmul12ad  9271  lemul12ad  9272  lemul12bd  9273  nndivre  9340  nndivtr  9346  halfaddsubcl  9538  halfaddsub  9539  lt2halves  9541  nnrecl  9561  elnn0nn  9605  elnnnn0b  9607  elnnnn0c  9608  nn0addge1  9609  nn0addge2  9610  xnn0xrnemnf  9642  elnn0z  9657  elnnz1  9667  nzadd  9697  elz2  9716  zdivadd  9735  zdivmul  9736  zextle  9737  peano2uz2  9753  uzind  9757  btwnz  9765  uzss  9943  eluzp1m1  9946  infregelbex  9998  eluz2b2  10003  qre  10025  qaddcl  10035  qmulcl  10037  qreccl  10042  irradd  10046  irrmul  10047  elpqb  10050  cnref1o  10051  rprege0  10069  rprene0  10072  rpreap0  10073  rpcnne0  10074  rpcnap0  10075  rpregt0d  10104  rprege0d  10105  rprene0d  10106  rpcnne0d  10107  lediv2ad  10120  ledivge1le  10127  lediv12ad  10157  nnledivrp  10167  nn0ledivnn  10168  xrlttri3  10199  xrrebnd  10221  xrrege0  10227  xnn0xadd0  10269  xlesubadd  10285  elioo4g  10336  ioomax  10350  iccmax  10351  divelunit  10404  elfz5  10420  uzsubsubfz  10452  fzopth  10467  fzass4  10468  fzrev2  10492  uzsplit  10499  elfz2nn0  10519  difelfzle  10541  1fv  10546  4fvwrd4  10547  fzo1fzo0n0  10595  elfzom1elp1fzo  10620  subfzo0  10661  infssuzex  10666  infssfzcldc  10669  infssfzledc  10670  qtri3or  10675  adddivflid  10727  flltdivnn0lt  10739  intfracq  10757  modqid2  10788  modfzo0difsn  10832  seq3val  10897  seqvalcd  10898  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemmo  10942  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seqf1oglem1  10956  seqf1oglem2  10957  expclzaplem  11000  leexp1a  11031  expubnd  11033  le2sq2  11052  sumsqeq0  11055  bernneq  11098  expnlbnd  11102  nn0opthd  11160  faclbnd6  11182  facavg  11184  sseqn  11279  hashfibclem  11282  hashf1lem2  11286  seq3coll  11294  hash2en  11295  wrdnval  11335  ccat0  11364  ccatsymb  11370  ccatalpha  11381  swrdspsleq  11439  pfxtrcfv  11465  pfxsuffeqwrdeq  11470  wrd2ind  11495  pfxccatin12lem2a  11499  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  pfxccatpfx1  11508  pfxccatpfx2  11509  swrdccatin1d  11515  swrdccatin2d  11516  shftlem  11581  shftfvalg  11583  shftfval  11586  cvg1nlemcau  11750  cvg1nlemres  11751  rexuz3  11756  resqrexlemcvg  11785  resqrexlemglsq  11788  resqrexlemga  11789  sqrtle  11802  sqrtlt  11803  sqrt11  11805  sqrtsq2  11809  absmul  11835  sqabs  11848  abslt  11854  absle  11855  lenegsq  11861  maxleastb  11980  maxltsup  11984  rexanre  11986  negfi  11994  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxltsup  12024  xrmaxadd  12027  climcn2  12075  mulcn2  12078  summodclem2a  12148  summodc  12150  fsum3  12154  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  fsump1i  12200  fsum0diaglem  12207  mptfzshft  12209  fsumrev  12210  fsummulc2  12215  fsum00  12229  expcnvap0  12269  mertenslemi1  12302  ntrivcvgap0  12316  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodrev  12386  fprodconst  12387  eftlub  12457  efieq  12502  sincos1sgn  12532  demoivreALT  12541  dvdsval3  12558  dvdscmul  12585  dvdsmulc  12586  dvdscmulr  12587  dvdsmulcr  12588  modmulconst  12590  dvds2ln  12591  ltoddhalfle  12660  nn0o  12674  divalg2  12693  ndvdssub  12697  ndvdsadd  12698  divgcdz  12748  gcd0id  12756  gcdaddm  12761  bezoutlemstep  12774  bezoutlemmain  12775  dfgcd3  12787  dfgcd2  12791  lcmcllem  12845  dvdslcm  12847  lcmgcdlem  12855  lcmgcdnn  12860  qredeq  12874  qredeu  12875  rpdvds  12877  divgcdcoprm0  12879  cncongr1  12881  cncongr2  12882  cncongrcoprm  12884  prmind2  12898  isprm5  12920  isprm6  12925  prmexpb  12929  cncongrprm  12935  sqrt2irrlem  12939  pw2dvdslemn  12943  oddpwdclemxy  12947  oddpwdclemdc  12951  oddpwdc  12952  hashdvds  12999  prmdiv  13013  hashgcdlem  13016  nnoddn2prmb  13041  pythagtriplem6  13049  pythagtriplem7  13050  pcpre1  13071  pccl  13078  pcmul  13080  pcdiv  13081  pcqmul  13082  pcqcl  13085  pcdvds  13094  pcndvds  13096  pcndvds2  13098  pc2dvds  13109  dvdsprmpweqle  13116  difsqpwdvds  13117  pcaddlem  13118  pcadd  13119  pcmptcl  13121  pcmpt  13122  fldivp1  13127  pcfac  13129  oddprmdvds  13133  infpnlem2  13139  4sqlem5  13161  4sqlem6  13162  4sqlem4a  13170  4sqexercise1  13177  4sqexercise2  13178  4sqlem13m  13182  4sqlem15  13184  4sqlem16  13185  ballotfilem2  13228  ballotfilemfp1  13231  ballotfilemsf1o  13257  ballotfilemrinv0  13276  ballotfilem7  13279  ballotfilemth  13281  ennnfonelemfun  13308  ennnfonelemim  13315  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  ctiunctlemfo  13330  omctfn  13334  fnpr2ob  13661  ismgmid2  13700  fngzsum  13708  gzsumvalx  13709  gzsumfzval  13711  gzsum0  13713  gzsumval2  13714  issgrpd  13727  ismndd  13750  imasmnd2  13759  mhmf1o  13777  subsubm  13790  dfgrp2  13832  isgrpid2  13845  isgrpinv  13859  grplrinv  13862  dfgrp3mlem  13903  dfgrp3m  13904  dfgrp3me  13905  imasgrp2  13913  mhmmnd  13919  issubg2m  13992  issubgrpd2  13993  grpissubg  13997  subsubg  14000  subgintm  14001  isnsg3  14010  nmzsubg  14013  eqgval  14026  eqgen  14030  isghmd  14055  ghmrn  14060  ghmpreima  14069  ghmf1o  14078  conjghm  14079  conjnmzb  14083  ghmpropd  14086  rinvmod  14113  imasabl  14140  gsumvalfi  14152  gsump1  14157  prdsidlem  14193  prdsinvlem  14196  rnglz  14244  isrngd  14252  rng1zr  14259  srgdilem  14273  srg1zr  14291  srglmhm  14297  srgrmhm  14298  ringdilem  14316  isringd  14346  ringsrg  14352  ringinvnzdiv  14355  imasring  14369  dvdsrd  14401  unitgrp  14423  isrim0  14468  isrhm2d  14472  rhmf1o  14475  rhmco  14481  rhmopp  14483  issubrng2  14518  subsubrng  14522  subrgugrp  14548  issubrg2  14549  subsubrg  14553  resrhm  14556  ringunitap  14593  aprap  14598  drngunitap  14608  lmodfopnelem2  14662  lsssubg  14714  islss3  14716  islss4  14719  ellspsn6  14745  lidlacl  14821  lidlsubg  14823  lidlrsppropdg  14832  2idlelbas  14853  cnfld1  14909  cnsubglem  14916  mulgghm2  14943  zndvds  14984  isassad  15011  issubassa  15013  assapropd  15014  psrbagcon  15062  mplsubgfi  15092  topgele  15130  tgcl  15165  epttop  15191  opnssneib  15257  iscnp4  15319  cnco  15322  cncnp  15331  cnrest2  15337  lmss  15347  txcnp  15372  txcn  15376  cnmpt12  15388  cnmpt22  15395  hmeof1o  15410  psmetres2  15434  distspace  15436  ismeti  15447  isxmetd  15448  xmetpsmet  15470  xblss2ps  15505  xblss2  15506  blcntrps  15516  blcntr  15517  blin2  15533  mopni3  15585  metequiv2  15597  bdmet  15603  xmettx  15611  cnbl0  15635  cnblcld  15636  tgioo  15655  elcncf1di  15680  dedekindeulemlu  15722  suplociccex  15726  dedekindicclemlu  15731  dedekindicc  15734  ivthinclemlopn  15737  ivthdec  15745  ivthreinc  15746  ivthdichlem  15752  cnplimcim  15768  limccnp2lem  15777  dvfvalap  15782  plymullem  15851  reeff1olem  15872  sin0pilem1  15882  pilem3  15884  ptolemy  15925  sincosq1sgn  15927  sinq12gt0  15931  ioocosf1o  15955  rprelogbmulexp  16058  pellexlem3  16093  perfectlem2  16114  lgslem3  16121  lgsne0  16157  gausslemma2dlem0b  16169  gausslemma2dlem0c  16170  lgsquadlem2  16197  lgsquad2lem2  16201  2lgsoddprmlem2  16225  2sqlem8  16242  gropd  16288  grstructd2dom  16289  incistruhgr  16331  umgrislfupgrenlem  16371  umgrislfupgrdom  16372  uspgrupgrushgr  16423  usgrumgruspgr  16426  usgruspgrben  16427  usgrislfuspgrdom  16431  umgrvad2edg  16452  umgr2edgneu  16453  ushgredgedg  16467  ushgredgedgloop  16469  subgrprop3  16503  iswlkg  16570  wlk2f  16592  upgriswlkdc  16601  wlkv0  16610  wlklenvclwlk  16614  wlkepvtx  16616  upgr2wlkdc  16618  wlkres  16620  clwwlkccatlem  16641  clwwlkccat  16642  clwwlknbp  16656  clwwlknp  16658  clwwlkext2edg  16663  clwwlknon  16670  clwwlknonccat  16674  clwwlknonex2  16680  clwwlknonex2e  16681  trlsegvdeglem1  16701  dichmul0orlem3  16755  bj-nnan  16764  bj-charfun  16833  bdop  16901  bdunexb  16946  bj-om  16963  findset  16971  bj-peano4  16981  bj-inf2vn  17000  bj-inf2vn2  17001  pwle2  17028  pwf1oexmid  17029  nnnninfex  17065  sbthom  17071  qdencn  17072  trilpolemlt1  17090