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  607  biadanid  618  ioran  760  ordi  824  stdcndc  853  stdcndcOLD  854  dfandc  892  mpbi2and  952  mpbir2and  953  pm4.82  959  pm4.83dc  960  rnlem  985  ifp2  989  syl22anc  1275  syl112anc  1278  syl121anc  1279  syl211anc  1280  syl23anc  1281  syl32anc  1282  syl122anc  1283  syl212anc  1284  syl221anc  1285  syl222anc  1290  syl123anc  1291  syl132anc  1292  syl213anc  1293  syl231anc  1294  syl312anc  1295  syl321anc  1296  syl223anc  1300  syl232anc  1301  syl322anc  1302  syl233anc  1303  syl323anc  1304  syl332anc  1305  ecased  1386  19.26  1530  nfand  1617  19.40  1680  equsexd  1778  sbcof2  1859  sbequ8  1896  eu2  2127  eu3h  2128  eu5  2130  mooran2  2156  datisi  2193  felapton  2197  darapti  2198  dimatis  2200  fresison  2201  fesapo  2203  reximssdv  2648  r19.26  2671  r19.29af2  2685  r19.40  2699  eqvinc  2943  eqvincg  2944  elrabd  2978  reu6  3009  reu3  3010  indifdir  3481  undif3ss  3486  un00  3559  eqifdc  3663  disjpr2  3758  prel12  3880  prneimg  3883  preqsn  3884  disjiun  4109  opth  4358  0nelop  4369  euotd  4376  opelopabsb  4383  ispod  4430  elon2  4502  unexb  4568  opeluu  4576  eusvnfb  4580  suc11g  4684  nlimsucg  4693  tfi  4709  vtoclr  4803  opthprc  4806  ideqg  4911  resiexg  5088  dminss  5182  imainss  5183  ssxpbm  5203  relrelss  5294  funopg  5391  fununfun  5404  fntpg  5417  fun11uni  5431  imain  5443  funimaexglem  5444  funssxp  5537  ffdm  5538  f00  5564  dffo2  5599  fodmrnu  5603  foco  5606  fun11iun  5640  f1o00  5656  fsnd  5664  fv3  5698  dff2  5826  dff3im  5827  dffo4  5830  ffnfv  5840  ffvresb  5845  fsn2  5856  fconstfvm  5907  fnfvima  5926  resfvresima  5929  fcof1o  5968  isocnv  5990  isotr  5995  riotaprop  6037  acexmidlemcase  6053  caovlem2d  6255  f1ocnvd  6265  f1o3d  6271  caofcom  6306  resfunexgALT  6310  elxp7  6377  2ndrn  6390  1stconst  6430  2ndconst  6431  cnvf1olem  6433  poxp  6441  ressuppss  6467  funsssuppss  6471  dftpos4  6507  dfsmo2  6531  tfrlem5  6558  tfrlemiex  6575  tfr1onlemsucaccv  6585  tfr1onlembfn  6588  tfr1onlemex  6591  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembfn  6601  tfrcllemex  6604  tfrcllemres  6606  tfrcl  6608  frecabex  6642  frecabcl  6643  frecfcllem  6648  frecrdg  6652  oawordi  6715  nntri3  6743  nntr2  6749  nnmordi  6762  iserd  6806  relelec  6822  erth  6826  qliftfun  6864  mapsnd  6936  mapsncnv  6943  mptelixpg  6982  bren  6996  pw2f1odclem  7100  mapunen  7117  findcard2d  7161  findcard2sd  7162  isinfinf  7167  tridc  7170  nnwetri  7189  undifdcss  7196  fiintim  7204  fisseneq  7208  fidcenumlemim  7235  sbthlemi9  7248  supisolem  7312  ordiso2  7339  updjud  7386  difinfsn  7404  ctssdccl  7415  nnnninfeq  7432  omniwomnimkv  7471  pr2cv  7507  acfun  7527  exmidontriimlem2  7542  onntri45  7564  dftap2  7581  netap  7584  2omotaplemap  7587  ccfunen  7594  cc4f  7599  cc4n  7601  elni2  7645  dfplpq2  7685  dfmpq2  7686  enqbreq2  7688  enqdc1  7693  addcmpblnq  7698  addclnq  7706  nqpi  7709  addassnqg  7713  mulassnqg  7715  mulcanenq  7716  distrnqg  7718  1qec  7719  recexnq  7721  subhalfnqq  7745  enq0tr  7765  nqnq0pi  7769  nq0nn  7773  mulcanenq0ec  7776  nnnq0lem1  7777  addclnq0  7782  distrnq0  7790  addassnq0lemcl  7792  elnp1st2nd  7807  prarloc  7834  addlocprlemlt  7862  addlocprlemeq  7864  addlocprlemgt  7865  addclpr  7868  nqprm  7873  mullocprlem  7901  mullocpr  7902  mulclpr  7903  ltpopr  7926  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemrnd  7936  ltexprlemdisj  7937  addcanprleml  7945  addcanprlemu  7946  addcanprg  7947  recexprlemm  7955  recexprlemopl  7956  recexprlemopu  7958  recexprlemrnd  7960  recexprlemdisj  7961  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemrnd  7981  cauappcvgprlemdisj  7982  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemrnd  8004  caucvgprlemlim  8012  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemm  8027  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemrnd  8032  caucvgprprlemexbt  8037  caucvgprprlemlim  8042  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  prsrlem1  8073  mulclsr  8085  mulasssrg  8089  distrsrg  8090  suplocsrlemb  8137  elreal2  8161  axmulass  8204  axdistr  8205  axcaucvglemcau  8229  add20  8765  mullt0  8771  rereim  8877  ltmul1  8883  cru  8893  mulap0r  8906  aprcl  8937  aptap  8941  divmuldivap  9003  divmuleqap  9008  divadddivap  9018  divmuldivapd  9123  divmuleqapd  9124  div2subap  9128  ltmul12a  9151  lemul12a  9153  lemulge11  9157  lediv12a  9185  lediv2a  9186  recgt1i  9189  recreclt  9191  ledivp1  9194  lemul1ad  9230  lemul2ad  9231  ltmul12ad  9232  lemul12ad  9233  lemul12bd  9234  nndivre  9290  nndivtr  9296  halfaddsubcl  9488  halfaddsub  9489  lt2halves  9491  nnrecl  9511  elnn0nn  9555  elnnnn0b  9557  elnnnn0c  9558  nn0addge1  9559  nn0addge2  9560  xnn0xrnemnf  9592  elnn0z  9607  elnnz1  9617  nzadd  9647  elz2  9666  zdivadd  9685  zdivmul  9686  zextle  9687  peano2uz2  9703  uzind  9707  btwnz  9715  uzss  9893  eluzp1m1  9896  infregelbex  9948  eluz2b2  9953  qre  9975  qaddcl  9985  qmulcl  9987  qreccl  9992  irradd  9996  irrmul  9997  elpqb  10000  cnref1o  10001  rprege0  10019  rprene0  10022  rpreap0  10023  rpcnne0  10024  rpcnap0  10025  rpregt0d  10054  rprege0d  10055  rprene0d  10056  rpcnne0d  10057  lediv2ad  10070  ledivge1le  10077  lediv12ad  10107  nnledivrp  10117  nn0ledivnn  10118  xrlttri3  10149  xrrebnd  10171  xrrege0  10177  xnn0xadd0  10219  xlesubadd  10235  elioo4g  10286  ioomax  10300  iccmax  10301  divelunit  10354  elfz5  10370  uzsubsubfz  10401  fzopth  10416  fzass4  10417  fzrev2  10441  uzsplit  10448  elfz2nn0  10468  difelfzle  10490  1fv  10495  4fvwrd4  10496  fzo1fzo0n0  10544  elfzom1elp1fzo  10569  subfzo0  10610  infssuzex  10615  infssfzcldc  10618  infssfzledc  10619  qtri3or  10624  adddivflid  10676  flltdivnn0lt  10688  intfracq  10706  modqid2  10737  modfzo0difsn  10781  seq3val  10846  seqvalcd  10847  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemmo  10891  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seqf1oglem1  10905  seqf1oglem2  10906  expclzaplem  10949  leexp1a  10980  expubnd  10982  le2sq2  11001  sumsqeq0  11004  bernneq  11047  expnlbnd  11051  nn0opthd  11109  faclbnd6  11131  facavg  11133  sseqn  11228  hashfibclem  11231  seq3coll  11239  hash2en  11240  wrdnval  11280  ccat0  11309  ccatsymb  11315  ccatalpha  11326  swrdspsleq  11384  pfxtrcfv  11410  pfxsuffeqwrdeq  11415  wrd2ind  11440  pfxccatin12lem2a  11444  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  pfxccatpfx1  11453  pfxccatpfx2  11454  swrdccatin1d  11460  swrdccatin2d  11461  shftlem  11526  shftfvalg  11528  shftfval  11531  cvg1nlemcau  11694  cvg1nlemres  11695  rexuz3  11700  resqrexlemcvg  11729  resqrexlemglsq  11732  resqrexlemga  11733  sqrtle  11746  sqrtlt  11747  sqrt11  11749  sqrtsq2  11753  absmul  11779  sqabs  11792  abslt  11798  absle  11799  lenegsq  11805  maxleastb  11924  maxltsup  11928  rexanre  11930  negfi  11938  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxltsup  11968  xrmaxadd  11971  climcn2  12019  mulcn2  12022  summodclem2a  12092  summodc  12094  fsum3  12098  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fsump1i  12144  fsum0diaglem  12151  mptfzshft  12153  fsumrev  12154  fsummulc2  12159  fsum00  12173  expcnvap0  12213  mertenslemi1  12246  ntrivcvgap0  12260  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodrev  12330  fprodconst  12331  eftlub  12401  efieq  12446  sincos1sgn  12476  demoivreALT  12485  dvdsval3  12502  dvdscmul  12529  dvdsmulc  12530  dvdscmulr  12531  dvdsmulcr  12532  modmulconst  12534  dvds2ln  12535  ltoddhalfle  12604  nn0o  12618  divalg2  12637  ndvdssub  12641  ndvdsadd  12642  divgcdz  12692  gcd0id  12700  gcdaddm  12705  bezoutlemstep  12718  bezoutlemmain  12719  dfgcd3  12731  dfgcd2  12735  lcmcllem  12789  dvdslcm  12791  lcmgcdlem  12799  lcmgcdnn  12804  qredeq  12818  qredeu  12819  rpdvds  12821  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  cncongrcoprm  12828  prmind2  12842  isprm5  12864  isprm6  12869  prmexpb  12873  cncongrprm  12879  sqrt2irrlem  12883  pw2dvdslemn  12887  oddpwdclemxy  12891  oddpwdclemdc  12895  oddpwdc  12896  hashdvds  12943  prmdiv  12957  hashgcdlem  12960  nnoddn2prmb  12985  pythagtriplem6  12993  pythagtriplem7  12994  pcpre1  13015  pccl  13022  pcmul  13024  pcdiv  13025  pcqmul  13026  pcqcl  13029  pcdvds  13038  pcndvds  13040  pcndvds2  13042  pc2dvds  13053  dvdsprmpweqle  13060  difsqpwdvds  13061  pcaddlem  13062  pcadd  13063  pcmptcl  13065  pcmpt  13066  fldivp1  13071  pcfac  13073  oddprmdvds  13077  infpnlem2  13083  4sqlem5  13105  4sqlem6  13106  4sqlem4a  13114  4sqexercise1  13121  4sqexercise2  13122  4sqlem13m  13126  4sqlem15  13128  4sqlem16  13129  ballotfilem2  13172  ballotfilemfp1  13175  ballotfilemsf1o  13201  ballotfilemrinv0  13220  ballotfilem7  13223  ballotfilemth  13225  ennnfonelemfun  13252  ennnfonelemim  13259  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  ctiunctlemfo  13274  omctfn  13278  fnpr2ob  13604  ismgmid2  13643  fngsum  13651  igsumvalx  13652  gsumfzval  13654  gsum0g  13659  gsumval2  13660  issgrpd  13675  ismndd  13698  imasmnd2  13707  mhmf1o  13725  subsubm  13738  dfgrp2  13782  isgrpid2  13795  isgrpinv  13809  grplrinv  13812  dfgrp3mlem  13853  dfgrp3m  13854  dfgrp3me  13855  imasgrp2  13863  mhmmnd  13869  issubg2m  13942  issubgrpd2  13943  grpissubg  13947  subsubg  13950  subgintm  13951  isnsg3  13960  nmzsubg  13963  eqgval  13976  eqgen  13980  isghmd  14005  ghmrn  14010  ghmpreima  14019  ghmf1o  14028  conjghm  14029  conjnmzb  14033  ghmpropd  14036  rinvmod  14062  imasabl  14089  gfsumval  14102  gfsump1  14108  prdsidlem  14135  prdsinvlem  14138  rnglz  14184  isrngd  14192  rng1zr  14199  srgdilem  14212  srg1zr  14230  srglmhm  14236  srgrmhm  14237  ringdilem  14255  isringd  14284  ringsrg  14290  ringinvnzdiv  14293  imasring  14307  dvdsrd  14339  unitgrp  14361  isrim0  14406  isrhm2d  14410  rhmf1o  14413  rhmco  14419  rhmopp  14421  issubrng2  14456  subsubrng  14460  subrgugrp  14486  issubrg2  14487  subsubrg  14491  resrhm  14494  ringunitap  14531  aprap  14536  drngunitap  14546  lmodfopnelem2  14599  lsssubg  14651  islss3  14653  islss4  14656  lspsnel6  14682  lidlacl  14758  lidlsubg  14760  lidlrsppropdg  14769  2idlelbas  14790  cnfld1  14846  cnsubglem  14853  mulgghm2  14882  zndvds  14923  psrbagcon  14952  mplsubgfi  14982  topgele  15020  tgcl  15055  epttop  15081  opnssneib  15147  iscnp4  15209  cnco  15212  cncnp  15221  cnrest2  15227  lmss  15237  txcnp  15262  txcn  15266  cnmpt12  15278  cnmpt22  15285  hmeof1o  15300  psmetres2  15324  distspace  15326  ismeti  15337  isxmetd  15338  xmetpsmet  15360  xblss2ps  15395  xblss2  15396  blcntrps  15406  blcntr  15407  blin2  15423  mopni3  15475  metequiv2  15487  bdmet  15493  xmettx  15501  cnbl0  15525  cnblcld  15526  tgioo  15545  elcncf1di  15570  dedekindeulemlu  15612  suplociccex  15616  dedekindicclemlu  15621  dedekindicc  15624  ivthinclemlopn  15627  ivthdec  15635  ivthreinc  15636  ivthdichlem  15642  cnplimcim  15658  limccnp2lem  15667  dvfvalap  15672  plymullem  15741  reeff1olem  15762  sin0pilem1  15772  pilem3  15774  ptolemy  15815  sincosq1sgn  15817  sinq12gt0  15821  ioocosf1o  15845  rprelogbmulexp  15947  pellexlem3  15973  perfectlem2  15994  lgslem3  16001  lgsne0  16037  gausslemma2dlem0b  16049  gausslemma2dlem0c  16050  lgsquadlem2  16077  lgsquad2lem2  16081  2lgsoddprmlem2  16105  2sqlem8  16122  gropd  16168  grstructd2dom  16169  incistruhgr  16211  umgrislfupgrenlem  16251  umgrislfupgrdom  16252  uspgrupgrushgr  16303  usgrumgruspgr  16306  usgruspgrben  16307  usgrislfuspgrdom  16311  umgrvad2edg  16332  umgr2edgneu  16333  ushgredgedg  16347  ushgredgedgloop  16349  subgrprop3  16383  iswlkg  16450  wlk2f  16472  upgriswlkdc  16481  wlkv0  16490  wlklenvclwlk  16494  wlkepvtx  16496  upgr2wlkdc  16498  wlkres  16500  clwwlkccatlem  16521  clwwlkccat  16522  clwwlknbp  16536  clwwlknp  16538  clwwlkext2edg  16543  clwwlknon  16550  clwwlknonccat  16554  clwwlknonex2  16560  clwwlknonex2e  16561  trlsegvdeglem1  16581  bj-nnan  16634  bj-charfun  16703  bdop  16771  bdunexb  16816  bj-om  16833  findset  16841  bj-peano4  16851  bj-inf2vn  16870  bj-inf2vn2  16871  pwle2  16898  pwf1oexmid  16899  nnnninfex  16926  sbthom  16932  qdencn  16933  trilpolemlt1  16951