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  4379  0nelop  4390  euotd  4397  opelopabsb  4404  ispod  4451  elon2  4523  unexb  4590  opeluu  4598  eusvnfb  4602  suc11g  4706  nlimsucg  4715  tfi  4731  vtoclr  4825  opthprc  4828  ideqg  4933  resiexg  5111  dminss  5205  imainss  5206  ssxpbm  5226  relrelss  5317  funopg  5414  fununfun  5427  fntpg  5440  fun11uni  5454  imain  5466  funimaexglem  5467  funssxp  5560  ffdm  5561  f00  5587  dffo2  5622  fodmrnu  5626  foco  5629  fun11iun  5663  f1o00  5679  fsnd  5687  fv3  5721  fvun1d  5774  fvun2d  5775  dff2  5855  dff3im  5856  dffo4  5859  ffnfv  5869  ffvresb  5874  fsn2  5885  fconstfvm  5936  fnfvima  5956  resfvresima  5959  fcof1o  5998  isocnv  6020  isotr  6025  riotaprop  6067  acexmidlemcase  6083  caovlem2d  6285  f1ocnvd  6295  f1o3d  6301  caofcom  6337  resfunexgALT  6341  elxp7  6408  2ndrn  6421  1stconst  6461  2ndconst  6462  cnvf1olem  6464  poxp  6472  ressuppss  6498  funsssuppss  6502  dftpos4  6538  dfsmo2  6562  tfrlem5  6589  tfrlemiex  6606  tfr1onlemsucaccv  6616  tfr1onlembfn  6619  tfr1onlemex  6622  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembfn  6632  tfrcllemex  6635  tfrcllemres  6637  tfrcl  6639  frecabex  6673  frecabcl  6674  frecfcllem  6679  frecrdg  6683  oawordi  6746  nntri3  6774  nntr2  6780  nnmordi  6793  iserd  6837  relelec  6853  erth  6857  qliftfun  6895  mapsnd  6974  mapsncnv  6981  mptelixpg  7020  bren  7034  pw2f1odclem  7138  mapunen  7155  findcard2d  7199  findcard2sd  7200  isinfinf  7205  tridc  7208  nnwetri  7227  undifdcss  7234  fiintim  7242  fisseneq  7246  fidcenumlemim  7274  sbthlemi9  7287  supisolem  7354  ordiso2  7381  updjud  7428  difinfsn  7446  ctssdccl  7457  nnnninfeq  7474  omniwomnimkv  7513  pr2cv  7549  acfun  7569  exmidontriimlem2  7584  onntri45  7606  dftap2  7623  netap  7626  2omotaplemap  7629  ccfunen  7636  cc4f  7641  cc4n  7643  elni2  7687  dfplpq2  7727  dfmpq2  7728  enqbreq2  7730  enqdc1  7735  addcmpblnq  7740  addclnq  7748  nqpi  7751  addassnqg  7755  mulassnqg  7757  mulcanenq  7758  distrnqg  7760  1qec  7761  recexnq  7763  subhalfnqq  7787  enq0tr  7807  nqnq0pi  7811  nq0nn  7815  mulcanenq0ec  7818  nnnq0lem1  7819  addclnq0  7824  distrnq0  7832  addassnq0lemcl  7834  elnp1st2nd  7849  prarloc  7876  addlocprlemlt  7904  addlocprlemeq  7906  addlocprlemgt  7907  addclpr  7910  nqprm  7915  mullocprlem  7943  mullocpr  7944  mulclpr  7945  ltpopr  7968  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemrnd  7978  ltexprlemdisj  7979  addcanprleml  7987  addcanprlemu  7988  addcanprg  7989  recexprlemm  7997  recexprlemopl  7998  recexprlemopu  8000  recexprlemrnd  8002  recexprlemdisj  8003  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemrnd  8023  cauappcvgprlemdisj  8024  cauappcvgprlemlim  8034  caucvgprlemnkj  8039  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemrnd  8046  caucvgprlemlim  8054  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemm  8069  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemrnd  8074  caucvgprprlemexbt  8079  caucvgprprlemlim  8084  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  prsrlem1  8115  mulclsr  8127  mulasssrg  8131  distrsrg  8132  suplocsrlemb  8179  elreal2  8203  axmulass  8246  axdistr  8247  axcaucvglemcau  8271  add20  8809  mullt0  8815  rereim  8922  ltmul1  8928  cru  8938  mulap0r  8951  aprcl  8982  aptap  8986  divmuldivap  9050  divmuleqap  9055  divadddivap  9065  divmuldivapd  9170  divmuleqapd  9171  div2subap  9175  ltmul12a  9198  lemul12a  9200  lemulge11  9204  lediv12a  9232  lediv2a  9233  recgt1i  9236  recreclt  9238  ledivp1  9241  lemul1ad  9277  lemul2ad  9278  ltmul12ad  9279  lemul12ad  9280  lemul12bd  9281  nndivre  9349  nndivtr  9355  halfaddsubcl  9549  halfaddsub  9550  lt2halves  9552  nnrecl  9572  elnn0nn  9616  elnnnn0b  9618  elnnnn0c  9619  nn0addge1  9620  nn0addge2  9621  xnn0xrnemnf  9653  elnn0z  9668  elnnz1  9678  nzadd  9708  elz2  9727  zdivadd  9746  zdivmul  9747  zextle  9748  peano2uz2  9764  uzind  9768  btwnz  9776  uzss  9959  eluzp1m1  9962  infregelbex  10014  eluz2b2  10019  qre  10041  qaddcl  10051  qmulcl  10053  qreccl  10058  irradd  10062  irraddap  10063  irrmul  10064  elpqb  10067  cnref1o  10068  rprege0  10086  rprene0  10089  rpreap0  10090  rpcnne0  10091  rpcnap0  10092  rpregt0d  10121  rprege0d  10122  rprene0d  10123  rpcnne0d  10124  lediv2ad  10137  ledivge1le  10144  lediv12ad  10174  nnledivrp  10184  nn0ledivnn  10185  xrlttri3  10216  xrrebnd  10238  xrrege0  10244  xnn0xadd0  10286  xlesubadd  10302  elioo4g  10353  ioomax  10367  iccmax  10368  divelunit  10421  elfz5  10437  uzsubsubfz  10469  fzopth  10484  fzass4  10485  fzrev2  10509  uzsplit  10516  elfz2nn0  10536  difelfzle  10558  1fv  10563  4fvwrd4  10564  fzo1fzo0n0  10612  elfzom1elp1fzo  10637  subfzo0  10678  infssuzex  10683  infssfzcldc  10686  infssfzledc  10687  qtri3or  10692  adddivflid  10748  flltdivnn0lt  10760  intfracq  10778  modqid2  10809  modfzo0difsn  10853  seq3val  10918  seqvalcd  10919  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemmo  10963  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seqf1oglem1  10977  seqf1oglem2  10978  expclzaplem  11021  leexp1a  11052  expubnd  11054  le2sq2  11073  sumsqeq0  11076  bernneq  11119  expnlbnd  11123  nn0sqdc  11168  nn0opthd  11182  faclbnd6  11204  facavg  11206  sseqn  11301  hashfibclem  11304  hashf1lem2  11308  seq3coll  11316  hash2en  11317  wrdnval  11357  ccat0  11386  ccatsymb  11392  ccatalpha  11403  swrdspsleq  11461  pfxtrcfv  11487  pfxsuffeqwrdeq  11492  wrd2ind  11517  pfxccatin12lem2a  11521  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  pfxccatpfx1  11530  pfxccatpfx2  11531  swrdccatin1d  11537  swrdccatin2d  11538  shftlem  11603  shftfvalg  11605  shftfval  11608  cvg1nlemcau  11772  cvg1nlemres  11773  rexuz3  11778  resqrexlemcvg  11807  resqrexlemglsq  11810  resqrexlemga  11811  sqrtle  11824  sqrtlt  11825  sqrt11  11827  sqrtsq2  11831  absmul  11857  sqabs  11871  abslt  11877  absle  11878  lenegsq  11884  maxleastb  12003  maxltsup  12007  rexanre  12009  negfi  12017  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxltsup  12049  xrmaxadd  12052  climcn2  12100  mulcn2  12103  summodclem2a  12173  summodc  12175  fsum3  12179  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  fsump1i  12225  fsum0diaglem  12232  mptfzshft  12234  fsumrev  12235  fsummulc2  12240  fsum00  12254  expcnvap0  12294  mertenslemi1  12327  ntrivcvgap0  12341  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodrev  12411  fprodconst  12412  eftlub  12482  efieq  12527  sincos1sgn  12557  demoivreALT  12566  dvdsval3  12583  dvdscmul  12610  dvdsmulc  12611  dvdscmulr  12612  dvdsmulcr  12613  modmulconst  12615  dvds2ln  12616  ltoddhalfle  12685  nn0o  12699  divalg2  12718  ndvdssub  12722  ndvdsadd  12723  divgcdz  12773  gcd0id  12781  gcdaddm  12786  bezoutlemstep  12799  bezoutlemmain  12800  dfgcd3  12812  dfgcd2  12816  lcmcllem  12870  dvdslcm  12872  lcmgcdlem  12880  lcmgcdnn  12885  qredeq  12899  qredeu  12900  rpdvds  12902  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  cncongrcoprm  12909  prmind2  12923  isprm5  12946  isprm6  12951  prmexpb  12955  cncongrprm  12961  sqrt2irrlem  12965  pwbdvdslemn  12969  nnmaxpwlemxy  12973  nnmaxpwlemparts  12977  nnmaxpw  12978  hashdvds  13028  prmdiv  13042  hashgcdlem  13045  nnoddn2prmb  13070  pythagtriplem6  13078  pythagtriplem7  13079  pcpre1  13100  pccl  13107  pcmul  13109  pcdiv  13110  pcqmul  13111  pcqcl  13114  pcdvds  13123  pcndvds  13125  pcndvds2  13127  pc2dvds  13138  dvdsprmpweqle  13145  difsqpwdvds  13146  pcaddlem  13147  pcadd  13148  pcmptcl  13150  pcmpt  13151  fldivp1  13156  pcfac  13158  oddprmdvds  13162  infpnlem2  13168  4sqlem5  13190  4sqlem6  13191  4sqlem4a  13199  4sqexercise1  13206  4sqexercise2  13207  4sqlem13m  13211  4sqlem15  13213  4sqlem16  13214  ballotfilem2  13286  ballotfilemfp1  13289  ballotfilemsf1o  13315  ballotfilemrinv0  13334  ballotfilem7  13337  ballotfilemth  13339  ennnfonelemfun  13366  ennnfonelemim  13373  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  ctiunctlemfo  13388  omctfn  13392  fnpr2ob  13720  ismgmid2  13759  fngzsum  13767  gzsumvalx  13768  gzsumfzval  13770  gzsum0  13772  gzsumval2  13773  issgrpd  13786  ismndd  13809  imasmnd2  13818  mhmf1o  13836  subsubm  13849  dfgrp2  13891  isgrpid2  13904  isgrpinv  13918  grplrinv  13921  dfgrp3mlem  13962  dfgrp3m  13963  dfgrp3me  13964  imasgrp2  13972  mhmmnd  13978  issubg2m  14051  issubgrpd2  14052  grpissubg  14056  subsubg  14059  subgintm  14060  isnsg3  14069  nmzsubg  14072  eqgval  14085  eqgen  14089  isghmd  14114  ghmrn  14119  ghmpreima  14128  ghmf1o  14137  conjghm  14138  conjnmzb  14142  ghmpropd  14145  cntzrcl  14159  rinvmod  14203  imasabl  14230  gsumvalfi  14242  gsump1  14247  prdsidlem  14300  prdsinvlem  14303  rnglz  14351  isrngd  14359  rng1zr  14366  srgdilem  14380  srg1zr  14398  srglmhm  14404  srgrmhm  14405  ringdilem  14423  isringd  14453  ringsrg  14459  ringinvnzdiv  14462  imasring  14478  dvdsrd  14510  unitgrp  14532  isrim0  14577  isrhm2d  14581  rhmf1o  14584  rhmco  14590  rhmopp  14592  issubrng2  14627  subsubrng  14631  subrgugrp  14657  issubrg2  14658  subsubrg  14662  resrhm  14665  ringunitap  14702  aprap  14707  drngunitap  14717  lmodfopnelem2  14771  lsssubg  14823  islss3  14825  islss4  14828  ellspsn6  14854  lidlacl  14930  lidlsubg  14932  lidlrsppropdg  14941  2idlelbas  14962  cnfld1  15018  cnsubglem  15025  mulgghm2  15052  zndvds  15093  isassad  15120  issubassa  15122  assapropd  15123  psrbagcon  15171  gsumbagdiaglem  15175  mplsubgfi  15217  topgele  15255  tgcl  15290  epttop  15316  opnssneib  15382  iscnp4  15444  cnco  15447  cncnp  15456  cnrest2  15462  lmss  15472  txcnp  15497  txcn  15501  cnmpt12  15513  cnmpt22  15520  hmeof1o  15535  psmetres2  15559  distspace  15561  ismeti  15572  isxmetd  15573  xmetpsmet  15595  xblss2ps  15630  xblss2  15631  blcntrps  15641  blcntr  15642  blin2  15658  mopni3  15710  metequiv2  15722  bdmet  15728  xmettx  15736  cnbl0  15760  cnblcld  15761  tgioo  15780  elcncf1di  15805  dedekindeulemlu  15847  suplociccex  15851  dedekindicclemlu  15856  dedekindicc  15859  ivthinclemlopn  15862  ivthdec  15870  ivthreinc  15871  ivthdichlem  15877  cnplimcim  15893  limccnp2lem  15902  dvfvalap  15907  plymullem  15976  reeff1olem  15997  sin0pilem1  16008  pilem3  16010  ptolemy  16051  sincosq1sgn  16053  sinq12gt0  16057  ioocosf1o  16082  rprelogbmulexp  16192  zprmlogbaplem2  16216  pellexlem3  16231  chtublem  16295  perfectlem2  16300  bcmono  16304  bclbnd  16307  bposlem5  16315  bposlem6  16316  lgslem3  16326  lgsne0  16362  gausslemma2dlem0b  16374  gausslemma2dlem0c  16375  lgsquadlem2  16402  lgsquad2lem2  16406  2lgsoddprmlem2  16430  2sqlem8  16447  gropd  16493  grstructd2dom  16494  incistruhgr  16536  umgrislfupgrenlem  16576  umgrislfupgrdom  16577  uspgrupgrushgr  16628  usgrumgruspgr  16631  usgruspgrben  16632  usgrislfuspgrdom  16636  umgrvad2edg  16657  umgr2edgneu  16658  ushgredgedg  16672  ushgredgedgloop  16674  subgrprop3  16708  iswlkg  16775  wlk2f  16797  upgriswlkdc  16806  wlkv0  16815  wlklenvclwlk  16819  wlkepvtx  16821  upgr2wlkdc  16823  wlkres  16825  clwwlkccatlem  16846  clwwlkccat  16847  clwwlknbp  16861  clwwlknp  16863  clwwlkext2edg  16868  clwwlknon  16875  clwwlknonccat  16879  clwwlknonex2  16885  clwwlknonex2e  16886  trlsegvdeglem1  16906  dichmul0orlem3  16960  bj-nnan  16969  bj-charfun  17038  bdop  17106  bdunexb  17151  bj-om  17168  findset  17176  bj-peano4  17186  bj-inf2vn  17205  bj-inf2vn2  17206  pwle2  17233  pwf1oexmid  17234  nnnninfex  17271  sbthom  17277  qdencn  17278  trilpolemlt1  17297