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  14277  prdsinvlem  14280  rnglz  14328  isrngd  14336  rng1zr  14343  srgdilem  14357  srg1zr  14375  srglmhm  14381  srgrmhm  14382  ringdilem  14400  isringd  14430  ringsrg  14436  ringinvnzdiv  14439  imasring  14453  dvdsrd  14485  unitgrp  14507  isrim0  14552  isrhm2d  14556  rhmf1o  14559  rhmco  14565  rhmopp  14567  issubrng2  14602  subsubrng  14606  subrgugrp  14632  issubrg2  14633  subsubrg  14637  resrhm  14640  ringunitap  14677  aprap  14682  drngunitap  14692  lmodfopnelem2  14746  lsssubg  14798  islss3  14800  islss4  14803  ellspsn6  14829  lidlacl  14905  lidlsubg  14907  lidlrsppropdg  14916  2idlelbas  14937  cnfld1  14993  cnsubglem  15000  mulgghm2  15027  zndvds  15068  isassad  15095  issubassa  15097  assapropd  15098  psrbagcon  15146  mplsubgfi  15183  topgele  15221  tgcl  15256  epttop  15282  opnssneib  15348  iscnp4  15410  cnco  15413  cncnp  15422  cnrest2  15428  lmss  15438  txcnp  15463  txcn  15467  cnmpt12  15479  cnmpt22  15486  hmeof1o  15501  psmetres2  15525  distspace  15527  ismeti  15538  isxmetd  15539  xmetpsmet  15561  xblss2ps  15596  xblss2  15597  blcntrps  15607  blcntr  15608  blin2  15624  mopni3  15676  metequiv2  15688  bdmet  15694  xmettx  15702  cnbl0  15726  cnblcld  15727  tgioo  15746  elcncf1di  15771  dedekindeulemlu  15813  suplociccex  15817  dedekindicclemlu  15822  dedekindicc  15825  ivthinclemlopn  15828  ivthdec  15836  ivthreinc  15837  ivthdichlem  15843  cnplimcim  15859  limccnp2lem  15868  dvfvalap  15873  plymullem  15942  reeff1olem  15963  sin0pilem1  15974  pilem3  15976  ptolemy  16017  sincosq1sgn  16019  sinq12gt0  16023  ioocosf1o  16047  rprelogbmulexp  16153  zprmlogbaplem2  16177  pellexlem3  16192  chtublem  16256  perfectlem2  16261  bcmono  16265  bclbnd  16268  bposlem5  16276  bposlem6  16277  lgslem3  16287  lgsne0  16323  gausslemma2dlem0b  16335  gausslemma2dlem0c  16336  lgsquadlem2  16363  lgsquad2lem2  16367  2lgsoddprmlem2  16391  2sqlem8  16408  gropd  16454  grstructd2dom  16455  incistruhgr  16497  umgrislfupgrenlem  16537  umgrislfupgrdom  16538  uspgrupgrushgr  16589  usgrumgruspgr  16592  usgruspgrben  16593  usgrislfuspgrdom  16597  umgrvad2edg  16618  umgr2edgneu  16619  ushgredgedg  16633  ushgredgedgloop  16635  subgrprop3  16669  iswlkg  16736  wlk2f  16758  upgriswlkdc  16767  wlkv0  16776  wlklenvclwlk  16780  wlkepvtx  16782  upgr2wlkdc  16784  wlkres  16786  clwwlkccatlem  16807  clwwlkccat  16808  clwwlknbp  16822  clwwlknp  16824  clwwlkext2edg  16829  clwwlknon  16836  clwwlknonccat  16840  clwwlknonex2  16846  clwwlknonex2e  16847  trlsegvdeglem1  16867  dichmul0orlem3  16921  bj-nnan  16930  bj-charfun  16999  bdop  17067  bdunexb  17112  bj-om  17129  findset  17137  bj-peano4  17147  bj-inf2vn  17166  bj-inf2vn2  17167  pwle2  17194  pwf1oexmid  17195  nnnninfex  17231  sbthom  17237  qdencn  17238  trilpolemlt1  17257