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  605  biadanid  616  ioran  757  ordi  821  stdcndc  850  stdcndcOLD  851  dfandc  889  mpbi2and  949  mpbir2and  950  pm4.82  956  pm4.83dc  957  rnlem  982  ifp2  986  syl22anc  1272  syl112anc  1275  syl121anc  1276  syl211anc  1277  syl23anc  1278  syl32anc  1279  syl122anc  1280  syl212anc  1281  syl221anc  1282  syl222anc  1287  syl123anc  1288  syl132anc  1289  syl213anc  1290  syl231anc  1291  syl312anc  1292  syl321anc  1293  syl223anc  1297  syl232anc  1298  syl322anc  1299  syl233anc  1300  syl323anc  1301  syl332anc  1302  ecased  1383  19.26  1527  nfand  1614  19.40  1677  equsexd  1775  sbcof2  1856  sbequ8  1893  eu2  2122  eu3h  2123  eu5  2125  mooran2  2151  datisi  2188  felapton  2192  darapti  2193  dimatis  2195  fresison  2196  fesapo  2198  reximssdv  2634  r19.26  2657  r19.29af2  2671  r19.40  2685  eqvinc  2927  eqvincg  2928  elrabd  2962  reu6  2993  reu3  2994  indifdir  3461  undif3ss  3466  un00  3539  eqifdc  3640  disjpr2  3731  prel12  3852  prneimg  3855  preqsn  3856  disjiun  4081  opth  4327  0nelop  4338  euotd  4345  opelopabsb  4352  ispod  4399  elon2  4471  unexb  4537  opeluu  4545  eusvnfb  4549  suc11g  4653  nlimsucg  4662  tfi  4678  vtoclr  4772  opthprc  4775  ideqg  4879  resiexg  5056  dminss  5149  imainss  5150  ssxpbm  5170  relrelss  5261  funopg  5358  fununfun  5370  fntpg  5383  fun11uni  5397  imain  5409  funimaexglem  5410  funssxp  5501  ffdm  5502  f00  5525  dffo2  5560  fodmrnu  5564  foco  5567  fun11iun  5601  f1o00  5616  fsnd  5624  fv3  5658  dff2  5787  dff3im  5788  dffo4  5791  ffnfv  5801  ffvresb  5806  fsn2  5817  fconstfvm  5867  fnfvima  5884  resfvresima  5886  fcof1o  5925  isocnv  5947  isotr  5952  riotaprop  5992  acexmidlemcase  6008  caovlem2d  6210  f1ocnvd  6220  caofcom  6261  resfunexgALT  6265  elxp7  6328  2ndrn  6341  1stconst  6381  2ndconst  6382  cnvf1olem  6384  poxp  6392  dftpos4  6424  dfsmo2  6448  tfrlem5  6475  tfrlemiex  6492  tfr1onlemsucaccv  6502  tfr1onlembfn  6505  tfr1onlemex  6508  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembfn  6518  tfrcllemex  6521  tfrcllemres  6523  tfrcl  6525  frecabex  6559  frecabcl  6560  frecfcllem  6565  frecrdg  6569  oawordi  6632  nntri3  6660  nntr2  6666  nnmordi  6679  iserd  6723  relelec  6739  erth  6743  qliftfun  6781  mapsncnv  6859  mptelixpg  6898  bren  6912  pw2f1odclem  7015  findcard2d  7073  findcard2sd  7074  isinfinf  7079  tridc  7082  nnwetri  7101  undifdcss  7108  fiintim  7116  fisseneq  7119  fidcenumlemim  7142  sbthlemi9  7155  supisolem  7198  ordiso2  7225  updjud  7272  difinfsn  7290  ctssdccl  7301  nnnninfeq  7318  omniwomnimkv  7357  pr2cv  7393  acfun  7412  exmidontriimlem2  7427  onntri45  7449  dftap2  7460  netap  7463  2omotaplemap  7466  ccfunen  7473  cc4f  7478  cc4n  7480  elni2  7524  dfplpq2  7564  dfmpq2  7565  enqbreq2  7567  enqdc1  7572  addcmpblnq  7577  addclnq  7585  nqpi  7588  addassnqg  7592  mulassnqg  7594  mulcanenq  7595  distrnqg  7597  1qec  7598  recexnq  7600  subhalfnqq  7624  enq0tr  7644  nqnq0pi  7648  nq0nn  7652  mulcanenq0ec  7655  nnnq0lem1  7656  addclnq0  7661  distrnq0  7669  addassnq0lemcl  7671  elnp1st2nd  7686  prarloc  7713  addlocprlemlt  7741  addlocprlemeq  7743  addlocprlemgt  7744  addclpr  7747  nqprm  7752  mullocprlem  7780  mullocpr  7781  mulclpr  7782  ltpopr  7805  ltaddpr  7807  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemrnd  7815  ltexprlemdisj  7816  addcanprleml  7824  addcanprlemu  7825  addcanprg  7826  recexprlemm  7834  recexprlemopl  7835  recexprlemopu  7837  recexprlemrnd  7839  recexprlemdisj  7840  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemopu  7858  cauappcvgprlemrnd  7860  cauappcvgprlemdisj  7861  cauappcvgprlemlim  7871  caucvgprlemnkj  7876  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemopu  7881  caucvgprlemrnd  7883  caucvgprlemlim  7891  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnjltk  7901  caucvgprprlemm  7906  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemrnd  7911  caucvgprprlemexbt  7916  caucvgprprlemlim  7921  suplocexprlemrl  7927  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  prsrlem1  7952  mulclsr  7964  mulasssrg  7968  distrsrg  7969  suplocsrlemb  8016  elreal2  8040  axmulass  8083  axdistr  8084  axcaucvglemcau  8108  add20  8644  mullt0  8650  rereim  8756  ltmul1  8762  cru  8772  mulap0r  8785  aprcl  8816  aptap  8820  divmuldivap  8882  divmuleqap  8887  divadddivap  8897  divmuldivapd  9002  divmuleqapd  9003  div2subap  9007  ltmul12a  9030  lemul12a  9032  lemulge11  9036  lediv12a  9064  lediv2a  9065  recgt1i  9068  recreclt  9070  ledivp1  9073  lemul1ad  9109  lemul2ad  9110  ltmul12ad  9111  lemul12ad  9112  lemul12bd  9113  nndivre  9169  nndivtr  9175  halfaddsubcl  9367  halfaddsub  9368  lt2halves  9370  nnrecl  9390  elnn0nn  9434  elnnnn0b  9436  elnnnn0c  9437  nn0addge1  9438  nn0addge2  9439  xnn0xrnemnf  9467  elnn0z  9482  elnnz1  9492  nzadd  9522  elz2  9541  zdivadd  9559  zdivmul  9560  zextle  9561  peano2uz2  9577  uzind  9581  btwnz  9589  uzss  9767  eluzp1m1  9770  infregelbex  9822  eluz2b2  9827  qre  9849  qaddcl  9859  qmulcl  9861  qreccl  9866  irradd  9870  irrmul  9871  elpqb  9874  cnref1o  9875  rprege0  9893  rprene0  9896  rpreap0  9897  rpcnne0  9898  rpcnap0  9899  rpregt0d  9928  rprege0d  9929  rprene0d  9930  rpcnne0d  9931  lediv2ad  9944  ledivge1le  9951  lediv12ad  9981  nnledivrp  9991  nn0ledivnn  9992  xrlttri3  10022  xrrebnd  10044  xrrege0  10050  xnn0xadd0  10092  xlesubadd  10108  elioo4g  10159  ioomax  10173  iccmax  10174  divelunit  10227  elfz5  10242  uzsubsubfz  10272  fzopth  10286  fzass4  10287  fzrev2  10310  uzsplit  10317  elfz2nn0  10337  difelfzle  10359  1fv  10364  4fvwrd4  10365  fzo1fzo0n0  10412  elfzom1elp1fzo  10437  subfzo0  10478  infssuzex  10483  qtri3or  10490  adddivflid  10542  flltdivnn0lt  10554  intfracq  10572  modqid2  10603  modfzo0difsn  10647  seq3val  10712  seqvalcd  10713  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemmo  10757  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seqf1oglem1  10771  seqf1oglem2  10772  expclzaplem  10815  leexp1a  10846  expubnd  10848  le2sq2  10867  sumsqeq0  10870  bernneq  10912  expnlbnd  10916  nn0opthd  10974  faclbnd6  10996  facavg  10998  seq3coll  11096  hash2en  11097  wrdnval  11134  ccat0  11163  ccatsymb  11169  ccatalpha  11180  swrdspsleq  11238  pfxtrcfv  11264  pfxsuffeqwrdeq  11269  wrd2ind  11294  pfxccatin12lem2a  11298  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  pfxccatpfx1  11307  pfxccatpfx2  11308  swrdccatin1d  11314  swrdccatin2d  11315  shftlem  11367  shftfvalg  11369  shftfval  11372  cvg1nlemcau  11535  cvg1nlemres  11536  rexuz3  11541  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  sqrtle  11587  sqrtlt  11588  sqrt11  11590  sqrtsq2  11594  absmul  11620  sqabs  11633  abslt  11639  absle  11640  lenegsq  11646  maxleastb  11765  maxltsup  11769  rexanre  11771  negfi  11779  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxltsup  11809  xrmaxadd  11812  climcn2  11860  mulcn2  11863  summodclem2a  11932  summodc  11934  fsum3  11938  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  fsump1i  11984  fsum0diaglem  11991  mptfzshft  11993  fsumrev  11994  fsummulc2  11999  fsum00  12013  expcnvap0  12053  mertenslemi1  12086  ntrivcvgap0  12100  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodrev  12170  fprodconst  12171  eftlub  12241  efieq  12286  sincos1sgn  12316  demoivreALT  12325  dvdsval3  12342  dvdscmul  12369  dvdsmulc  12370  dvdscmulr  12371  dvdsmulcr  12372  modmulconst  12374  dvds2ln  12375  ltoddhalfle  12444  nn0o  12458  divalg2  12477  ndvdssub  12481  ndvdsadd  12482  divgcdz  12532  gcd0id  12540  gcdaddm  12545  bezoutlemstep  12558  bezoutlemmain  12559  dfgcd3  12571  dfgcd2  12575  lcmcllem  12629  dvdslcm  12631  lcmgcdlem  12639  lcmgcdnn  12644  qredeq  12658  qredeu  12659  rpdvds  12661  divgcdcoprm0  12663  cncongr1  12665  cncongr2  12666  cncongrcoprm  12668  prmind2  12682  isprm5  12704  isprm6  12709  prmexpb  12713  cncongrprm  12719  sqrt2irrlem  12723  pw2dvdslemn  12727  oddpwdclemxy  12731  oddpwdclemdc  12735  oddpwdc  12736  hashdvds  12783  prmdiv  12797  hashgcdlem  12800  nnoddn2prmb  12825  pythagtriplem6  12833  pythagtriplem7  12834  pcpre1  12855  pccl  12862  pcmul  12864  pcdiv  12865  pcqmul  12866  pcqcl  12869  pcdvds  12878  pcndvds  12880  pcndvds2  12882  pc2dvds  12893  dvdsprmpweqle  12900  difsqpwdvds  12901  pcaddlem  12902  pcadd  12903  pcmptcl  12905  pcmpt  12906  fldivp1  12911  pcfac  12913  oddprmdvds  12917  infpnlem2  12923  4sqlem5  12945  4sqlem6  12946  4sqlem4a  12954  4sqexercise1  12961  4sqexercise2  12962  4sqlem13m  12966  4sqlem15  12968  4sqlem16  12969  ennnfonelemfun  13028  ennnfonelemim  13035  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  ctiunctlemfo  13050  omctfn  13054  fnpr2ob  13413  ismgmid2  13453  fngsum  13461  igsumvalx  13462  gsumfzval  13464  gsum0g  13469  gsumval2  13470  issgrpd  13485  ismndd  13510  prdsidlem  13520  imasmnd2  13525  mhmf1o  13543  subsubm  13556  dfgrp2  13600  isgrpid2  13613  isgrpinv  13627  grplrinv  13630  dfgrp3mlem  13671  dfgrp3m  13672  dfgrp3me  13673  prdsinvlem  13681  imasgrp2  13687  mhmmnd  13693  issubg2m  13766  issubgrpd2  13767  grpissubg  13771  subsubg  13774  subgintm  13775  isnsg3  13784  nmzsubg  13787  eqgval  13800  eqgen  13804  isghmd  13829  ghmrn  13834  ghmpreima  13843  ghmf1o  13852  conjghm  13853  conjnmzb  13857  ghmpropd  13860  rinvmod  13886  imasabl  13913  rnglz  13948  isrngd  13956  srgdilem  13972  srglmhm  13996  srgrmhm  13997  ringdilem  14015  isringd  14044  ringsrg  14050  ringinvnzdiv  14053  imasring  14067  dvdsrd  14098  unitgrp  14120  isrim0  14165  isrhm2d  14169  rhmf1o  14172  rhmco  14178  rhmopp  14180  issubrng2  14214  subsubrng  14218  subrgugrp  14244  issubrg2  14245  subsubrg  14249  resrhm  14252  aprap  14290  lmodfopnelem2  14329  lsssubg  14381  islss3  14383  islss4  14386  lspsnel6  14412  lidlacl  14488  lidlsubg  14490  lidlrsppropdg  14499  2idlelbas  14520  cnfld1  14576  cnsubglem  14583  mulgghm2  14612  zndvds  14653  mplsubgfi  14705  topgele  14743  tgcl  14778  epttop  14804  opnssneib  14870  iscnp4  14932  cnco  14935  cncnp  14944  cnrest2  14950  lmss  14960  txcnp  14985  txcn  14989  cnmpt12  15001  cnmpt22  15008  hmeof1o  15023  psmetres2  15047  distspace  15049  ismeti  15060  isxmetd  15061  xmetpsmet  15083  xblss2ps  15118  xblss2  15119  blcntrps  15129  blcntr  15130  blin2  15146  mopni3  15198  metequiv2  15210  bdmet  15216  xmettx  15224  cnbl0  15248  cnblcld  15249  tgioo  15268  elcncf1di  15293  dedekindeulemlu  15335  suplociccex  15339  dedekindicclemlu  15344  dedekindicc  15347  ivthinclemlopn  15350  ivthdec  15358  ivthreinc  15359  ivthdichlem  15365  cnplimcim  15381  limccnp2lem  15390  dvfvalap  15395  plymullem  15464  reeff1olem  15485  sin0pilem1  15495  pilem3  15497  ptolemy  15538  sincosq1sgn  15540  sinq12gt0  15544  ioocosf1o  15568  rprelogbmulexp  15670  perfectlem2  15714  lgslem3  15721  lgsne0  15757  gausslemma2dlem0b  15769  gausslemma2dlem0c  15770  lgsquadlem2  15797  lgsquad2lem2  15801  2lgsoddprmlem2  15825  2sqlem8  15842  gropd  15888  grstructd2dom  15889  incistruhgr  15931  umgrislfupgrenlem  15969  umgrislfupgrdom  15970  uspgrupgrushgr  16021  usgrumgruspgr  16024  usgruspgrben  16025  usgrislfuspgrdom  16029  umgrvad2edg  16050  umgr2edgneu  16051  ushgredgedg  16065  ushgredgedgloop  16067  iswlkg  16126  wlk2f  16148  upgriswlkdc  16157  wlkv0  16166  wlklenvclwlk  16170  upgr2wlkdc  16172  wlkres  16174  clwwlkccatlem  16195  clwwlkccat  16196  clwwlknbp  16210  clwwlknp  16212  clwwlkext2edg  16217  clwwlknon  16224  clwwlknonccat  16228  clwwlknonex2  16234  clwwlknonex2e  16235  bj-nnan  16268  bj-charfun  16338  bdop  16406  bdunexb  16451  bj-om  16468  findset  16476  bj-peano4  16486  bj-inf2vn  16505  bj-inf2vn2  16506  pwle2  16535  pwf1oexmid  16536  nnnninfex  16560  sbthom  16566  qdencn  16567  trilpolemlt1  16581