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  7349  ordiso2  7376  updjud  7423  difinfsn  7441  ctssdccl  7452  nnnninfeq  7469  omniwomnimkv  7508  pr2cv  7544  acfun  7564  exmidontriimlem2  7579  onntri45  7601  dftap2  7618  netap  7621  2omotaplemap  7624  ccfunen  7631  cc4f  7636  cc4n  7638  elni2  7682  dfplpq2  7722  dfmpq2  7723  enqbreq2  7725  enqdc1  7730  addcmpblnq  7735  addclnq  7743  nqpi  7746  addassnqg  7750  mulassnqg  7752  mulcanenq  7753  distrnqg  7755  1qec  7756  recexnq  7758  subhalfnqq  7782  enq0tr  7802  nqnq0pi  7806  nq0nn  7810  mulcanenq0ec  7813  nnnq0lem1  7814  addclnq0  7819  distrnq0  7827  addassnq0lemcl  7829  elnp1st2nd  7844  prarloc  7871  addlocprlemlt  7899  addlocprlemeq  7901  addlocprlemgt  7902  addclpr  7905  nqprm  7910  mullocprlem  7938  mullocpr  7939  mulclpr  7940  ltpopr  7963  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemrnd  7973  ltexprlemdisj  7974  addcanprleml  7982  addcanprlemu  7983  addcanprg  7984  recexprlemm  7992  recexprlemopl  7993  recexprlemopu  7995  recexprlemrnd  7997  recexprlemdisj  7998  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemrnd  8018  cauappcvgprlemdisj  8019  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemrnd  8041  caucvgprlemlim  8049  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnjltk  8059  caucvgprprlemm  8064  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemrnd  8069  caucvgprprlemexbt  8074  caucvgprprlemlim  8079  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  prsrlem1  8110  mulclsr  8122  mulasssrg  8126  distrsrg  8127  suplocsrlemb  8174  elreal2  8198  axmulass  8241  axdistr  8242  axcaucvglemcau  8266  add20  8804  mullt0  8810  rereim  8917  ltmul1  8923  cru  8933  mulap0r  8946  aprcl  8977  aptap  8981  divmuldivap  9045  divmuleqap  9050  divadddivap  9060  divmuldivapd  9165  divmuleqapd  9166  div2subap  9170  ltmul12a  9193  lemul12a  9195  lemulge11  9199  lediv12a  9227  lediv2a  9228  recgt1i  9231  recreclt  9233  ledivp1  9236  lemul1ad  9272  lemul2ad  9273  ltmul12ad  9274  lemul12ad  9275  lemul12bd  9276  nndivre  9343  nndivtr  9349  halfaddsubcl  9543  halfaddsub  9544  lt2halves  9546  nnrecl  9566  elnn0nn  9610  elnnnn0b  9612  elnnnn0c  9613  nn0addge1  9614  nn0addge2  9615  xnn0xrnemnf  9647  elnn0z  9662  elnnz1  9672  nzadd  9702  elz2  9721  zdivadd  9740  zdivmul  9741  zextle  9742  peano2uz2  9758  uzind  9762  btwnz  9770  uzss  9953  eluzp1m1  9956  infregelbex  10008  eluz2b2  10013  qre  10035  qaddcl  10045  qmulcl  10047  qreccl  10052  irradd  10056  irraddap  10057  irrmul  10058  elpqb  10061  cnref1o  10062  rprege0  10080  rprene0  10083  rpreap0  10084  rpcnne0  10085  rpcnap0  10086  rpregt0d  10115  rprege0d  10116  rprene0d  10117  rpcnne0d  10118  lediv2ad  10131  ledivge1le  10138  lediv12ad  10168  nnledivrp  10178  nn0ledivnn  10179  xrlttri3  10210  xrrebnd  10232  xrrege0  10238  xnn0xadd0  10280  xlesubadd  10296  elioo4g  10347  ioomax  10361  iccmax  10362  divelunit  10415  elfz5  10431  uzsubsubfz  10463  fzopth  10478  fzass4  10479  fzrev2  10503  uzsplit  10510  elfz2nn0  10530  difelfzle  10552  1fv  10557  4fvwrd4  10558  fzo1fzo0n0  10606  elfzom1elp1fzo  10631  subfzo0  10672  infssuzex  10677  infssfzcldc  10680  infssfzledc  10681  qtri3or  10686  adddivflid  10742  flltdivnn0lt  10754  intfracq  10772  modqid2  10803  modfzo0difsn  10847  seq3val  10912  seqvalcd  10913  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemmo  10957  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seqf1oglem1  10971  seqf1oglem2  10972  expclzaplem  11015  leexp1a  11046  expubnd  11048  le2sq2  11067  sumsqeq0  11070  bernneq  11113  expnlbnd  11117  nn0sqdc  11162  nn0opthd  11176  faclbnd6  11198  facavg  11200  sseqn  11295  hashfibclem  11298  hashf1lem2  11302  seq3coll  11310  hash2en  11311  wrdnval  11351  ccat0  11380  ccatsymb  11386  ccatalpha  11397  swrdspsleq  11455  pfxtrcfv  11481  pfxsuffeqwrdeq  11486  wrd2ind  11511  pfxccatin12lem2a  11515  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  pfxccatpfx1  11524  pfxccatpfx2  11525  swrdccatin1d  11531  swrdccatin2d  11532  shftlem  11597  shftfvalg  11599  shftfval  11602  cvg1nlemcau  11766  cvg1nlemres  11767  rexuz3  11772  resqrexlemcvg  11801  resqrexlemglsq  11804  resqrexlemga  11805  sqrtle  11818  sqrtlt  11819  sqrt11  11821  sqrtsq2  11825  absmul  11851  sqabs  11865  abslt  11871  absle  11872  lenegsq  11878  maxleastb  11997  maxltsup  12001  rexanre  12003  negfi  12011  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxltsup  12043  xrmaxadd  12046  climcn2  12094  mulcn2  12097  summodclem2a  12167  summodc  12169  fsum3  12173  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  fsump1i  12219  fsum0diaglem  12226  mptfzshft  12228  fsumrev  12229  fsummulc2  12234  fsum00  12248  expcnvap0  12288  mertenslemi1  12321  ntrivcvgap0  12335  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodrev  12405  fprodconst  12406  eftlub  12476  efieq  12521  sincos1sgn  12551  demoivreALT  12560  dvdsval3  12577  dvdscmul  12604  dvdsmulc  12605  dvdscmulr  12606  dvdsmulcr  12607  modmulconst  12609  dvds2ln  12610  ltoddhalfle  12679  nn0o  12693  divalg2  12712  ndvdssub  12716  ndvdsadd  12717  divgcdz  12767  gcd0id  12775  gcdaddm  12780  bezoutlemstep  12793  bezoutlemmain  12794  dfgcd3  12806  dfgcd2  12810  lcmcllem  12864  dvdslcm  12866  lcmgcdlem  12874  lcmgcdnn  12879  qredeq  12893  qredeu  12894  rpdvds  12896  divgcdcoprm0  12898  cncongr1  12900  cncongr2  12901  cncongrcoprm  12903  prmind2  12917  isprm5  12940  isprm6  12945  prmexpb  12949  cncongrprm  12955  sqrt2irrlem  12959  pwbdvdslemn  12963  nnmaxpwlemxy  12967  nnmaxpwlemparts  12971  nnmaxpw  12972  hashdvds  13022  prmdiv  13036  hashgcdlem  13039  nnoddn2prmb  13064  pythagtriplem6  13072  pythagtriplem7  13073  pcpre1  13094  pccl  13101  pcmul  13103  pcdiv  13104  pcqmul  13105  pcqcl  13108  pcdvds  13117  pcndvds  13119  pcndvds2  13121  pc2dvds  13132  dvdsprmpweqle  13139  difsqpwdvds  13140  pcaddlem  13141  pcadd  13142  pcmptcl  13144  pcmpt  13145  fldivp1  13150  pcfac  13152  oddprmdvds  13156  infpnlem2  13162  4sqlem5  13184  4sqlem6  13185  4sqlem4a  13193  4sqexercise1  13200  4sqexercise2  13201  4sqlem13m  13205  4sqlem15  13207  4sqlem16  13208  ballotfilem2  13280  ballotfilemfp1  13283  ballotfilemsf1o  13309  ballotfilemrinv0  13328  ballotfilem7  13331  ballotfilemth  13333  ennnfonelemfun  13360  ennnfonelemim  13367  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  ctiunctlemfo  13382  omctfn  13386  fnpr2ob  13714  ismgmid2  13753  fngzsum  13761  gzsumvalx  13762  gzsumfzval  13764  gzsum0  13766  gzsumval2  13767  issgrpd  13780  ismndd  13803  imasmnd2  13812  mhmf1o  13830  subsubm  13843  dfgrp2  13885  isgrpid2  13898  isgrpinv  13912  grplrinv  13915  dfgrp3mlem  13956  dfgrp3m  13957  dfgrp3me  13958  imasgrp2  13966  mhmmnd  13972  issubg2m  14045  issubgrpd2  14046  grpissubg  14050  subsubg  14053  subgintm  14054  isnsg3  14063  nmzsubg  14066  eqgval  14079  eqgen  14083  isghmd  14108  ghmrn  14113  ghmpreima  14122  ghmf1o  14131  conjghm  14132  conjnmzb  14136  ghmpropd  14139  cntzrcl  14153  rinvmod  14197  imasabl  14224  gsumvalfi  14236  gsump1  14241  prdsidlem  14284  prdsinvlem  14287  rnglz  14335  isrngd  14343  rng1zr  14350  srgdilem  14364  srg1zr  14382  srglmhm  14388  srgrmhm  14389  ringdilem  14407  isringd  14437  ringsrg  14443  ringinvnzdiv  14446  imasring  14460  dvdsrd  14492  unitgrp  14514  isrim0  14559  isrhm2d  14563  rhmf1o  14566  rhmco  14572  rhmopp  14574  issubrng2  14609  subsubrng  14613  subrgugrp  14639  issubrg2  14640  subsubrg  14644  resrhm  14647  ringunitap  14684  aprap  14689  drngunitap  14699  lmodfopnelem2  14753  lsssubg  14805  islss3  14807  islss4  14810  ellspsn6  14836  lidlacl  14912  lidlsubg  14914  lidlrsppropdg  14923  2idlelbas  14944  cnfld1  15000  cnsubglem  15007  mulgghm2  15034  zndvds  15075  isassad  15102  issubassa  15104  assapropd  15105  psrbagcon  15153  mplsubgfi  15191  topgele  15229  tgcl  15264  epttop  15290  opnssneib  15356  iscnp4  15418  cnco  15421  cncnp  15430  cnrest2  15436  lmss  15446  txcnp  15471  txcn  15475  cnmpt12  15487  cnmpt22  15494  hmeof1o  15509  psmetres2  15533  distspace  15535  ismeti  15546  isxmetd  15547  xmetpsmet  15569  xblss2ps  15604  xblss2  15605  blcntrps  15615  blcntr  15616  blin2  15632  mopni3  15684  metequiv2  15696  bdmet  15702  xmettx  15710  cnbl0  15734  cnblcld  15735  tgioo  15754  elcncf1di  15779  dedekindeulemlu  15821  suplociccex  15825  dedekindicclemlu  15830  dedekindicc  15833  ivthinclemlopn  15836  ivthdec  15844  ivthreinc  15845  ivthdichlem  15851  cnplimcim  15867  limccnp2lem  15876  dvfvalap  15881  plymullem  15950  reeff1olem  15971  sin0pilem1  15982  pilem3  15984  ptolemy  16025  sincosq1sgn  16027  sinq12gt0  16031  ioocosf1o  16056  rprelogbmulexp  16166  zprmlogbaplem2  16190  pellexlem3  16205  chtublem  16269  perfectlem2  16274  bcmono  16278  bclbnd  16281  bposlem5  16289  bposlem6  16290  lgslem3  16300  lgsne0  16336  gausslemma2dlem0b  16348  gausslemma2dlem0c  16349  lgsquadlem2  16376  lgsquad2lem2  16380  2lgsoddprmlem2  16404  2sqlem8  16421  gropd  16467  grstructd2dom  16468  incistruhgr  16510  umgrislfupgrenlem  16550  umgrislfupgrdom  16551  uspgrupgrushgr  16602  usgrumgruspgr  16605  usgruspgrben  16606  usgrislfuspgrdom  16610  umgrvad2edg  16631  umgr2edgneu  16632  ushgredgedg  16646  ushgredgedgloop  16648  subgrprop3  16682  iswlkg  16749  wlk2f  16771  upgriswlkdc  16780  wlkv0  16789  wlklenvclwlk  16793  wlkepvtx  16795  upgr2wlkdc  16797  wlkres  16799  clwwlkccatlem  16820  clwwlkccat  16821  clwwlknbp  16835  clwwlknp  16837  clwwlkext2edg  16842  clwwlknon  16849  clwwlknonccat  16853  clwwlknonex2  16859  clwwlknonex2e  16860  trlsegvdeglem1  16880  dichmul0orlem3  16934  bj-nnan  16943  bj-charfun  17012  bdop  17080  bdunexb  17125  bj-om  17142  findset  17150  bj-peano4  17160  bj-inf2vn  17179  bj-inf2vn2  17180  pwle2  17207  pwf1oexmid  17208  nnnninfex  17244  sbthom  17250  qdencn  17251  trilpolemlt1  17270