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  603  biadanid  614  ioran  753  ordi  817  stdcndc  846  stdcndcOLD  847  dfandc  885  mpbi2and  945  mpbir2and  946  pm4.82  952  pm4.83dc  953  rnlem  978  syl22anc  1250  syl112anc  1253  syl121anc  1254  syl211anc  1255  syl23anc  1256  syl32anc  1257  syl122anc  1258  syl212anc  1259  syl221anc  1260  syl222anc  1265  syl123anc  1266  syl132anc  1267  syl213anc  1268  syl231anc  1269  syl312anc  1270  syl321anc  1271  syl223anc  1275  syl232anc  1276  syl322anc  1277  syl233anc  1278  syl323anc  1279  syl332anc  1280  ecased  1361  19.26  1503  nfand  1590  19.40  1653  equsexd  1751  sbcof2  1832  sbequ8  1869  eu2  2097  eu3h  2098  eu5  2100  mooran2  2126  datisi  2163  felapton  2167  darapti  2168  dimatis  2170  fresison  2171  fesapo  2173  reximssdv  2609  r19.26  2631  r19.29af2  2645  r19.40  2659  eqvinc  2895  eqvincg  2896  elrabd  2930  reu6  2961  reu3  2962  indifdir  3428  undif3ss  3433  un00  3506  eqifdc  3606  disjpr2  3696  prel12  3811  prneimg  3814  preqsn  3815  disjiun  4038  opth  4280  0nelop  4291  euotd  4298  opelopabsb  4305  ispod  4350  elon2  4422  unexb  4488  opeluu  4496  eusvnfb  4500  suc11g  4604  nlimsucg  4613  tfi  4629  vtoclr  4722  opthprc  4725  ideqg  4828  resiexg  5003  dminss  5096  imainss  5097  ssxpbm  5117  relrelss  5208  funopg  5304  fununfun  5316  fntpg  5329  fun11uni  5343  imain  5355  funimaexglem  5356  funssxp  5444  ffdm  5445  f00  5466  dffo2  5501  fodmrnu  5505  foco  5508  fun11iun  5542  f1o00  5556  fsnd  5564  fv3  5598  dff2  5723  dff3im  5724  dffo4  5727  ffnfv  5737  ffvresb  5742  fsn2  5753  fconstfvm  5801  fnfvima  5818  fcof1o  5857  isocnv  5879  isotr  5884  riotaprop  5922  acexmidlemcase  5938  caovlem2d  6138  f1ocnvd  6147  caofcom  6188  resfunexgALT  6192  elxp7  6255  2ndrn  6268  1stconst  6306  2ndconst  6307  cnvf1olem  6309  poxp  6317  dftpos4  6348  dfsmo2  6372  tfrlem5  6399  tfrlemiex  6416  tfr1onlemsucaccv  6426  tfr1onlembfn  6429  tfr1onlemex  6432  tfr1onlemres  6434  tfrcllemsucaccv  6439  tfrcllembfn  6442  tfrcllemex  6445  tfrcllemres  6447  tfrcl  6449  frecabex  6483  frecabcl  6484  frecfcllem  6489  frecrdg  6493  oawordi  6554  nntri3  6582  nntr2  6588  nnmordi  6601  iserd  6645  relelec  6661  erth  6665  qliftfun  6703  mapsncnv  6781  mptelixpg  6820  bren  6834  pw2f1odclem  6930  findcard2d  6987  findcard2sd  6988  isinfinf  6993  tridc  6995  nnwetri  7012  undifdcss  7019  fiintim  7027  fisseneq  7030  fidcenumlemim  7053  sbthlemi9  7066  supisolem  7109  ordiso2  7136  updjud  7183  difinfsn  7201  ctssdccl  7212  nnnninfeq  7229  omniwomnimkv  7268  acfun  7318  exmidontriimlem2  7333  onntri45  7352  dftap2  7362  netap  7365  2omotaplemap  7368  ccfunen  7375  cc4f  7380  cc4n  7382  elni2  7426  dfplpq2  7466  dfmpq2  7467  enqbreq2  7469  enqdc1  7474  addcmpblnq  7479  addclnq  7487  nqpi  7490  addassnqg  7494  mulassnqg  7496  mulcanenq  7497  distrnqg  7499  1qec  7500  recexnq  7502  subhalfnqq  7526  enq0tr  7546  nqnq0pi  7550  nq0nn  7554  mulcanenq0ec  7557  nnnq0lem1  7558  addclnq0  7563  distrnq0  7571  addassnq0lemcl  7573  elnp1st2nd  7588  prarloc  7615  addlocprlemlt  7643  addlocprlemeq  7645  addlocprlemgt  7646  addclpr  7649  nqprm  7654  mullocprlem  7682  mullocpr  7683  mulclpr  7684  ltpopr  7707  ltaddpr  7709  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemrnd  7717  ltexprlemdisj  7718  addcanprleml  7726  addcanprlemu  7727  addcanprg  7728  recexprlemm  7736  recexprlemopl  7737  recexprlemopu  7739  recexprlemrnd  7741  recexprlemdisj  7742  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemopu  7760  cauappcvgprlemrnd  7762  cauappcvgprlemdisj  7763  cauappcvgprlemlim  7773  caucvgprlemnkj  7778  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemopu  7783  caucvgprlemrnd  7785  caucvgprlemlim  7793  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnjltk  7803  caucvgprprlemm  7808  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemrnd  7813  caucvgprprlemexbt  7818  caucvgprprlemlim  7823  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemex  7834  suplocexprlemub  7835  prsrlem1  7854  mulclsr  7866  mulasssrg  7870  distrsrg  7871  suplocsrlemb  7918  elreal2  7942  axmulass  7985  axdistr  7986  axcaucvglemcau  8010  add20  8546  mullt0  8552  rereim  8658  ltmul1  8664  cru  8674  mulap0r  8687  aprcl  8718  aptap  8722  divmuldivap  8784  divmuleqap  8789  divadddivap  8799  divmuldivapd  8904  divmuleqapd  8905  div2subap  8909  ltmul12a  8932  lemul12a  8934  lemulge11  8938  lediv12a  8966  lediv2a  8967  recgt1i  8970  recreclt  8972  ledivp1  8975  lemul1ad  9011  lemul2ad  9012  ltmul12ad  9013  lemul12ad  9014  lemul12bd  9015  nndivre  9071  nndivtr  9077  halfaddsubcl  9269  halfaddsub  9270  lt2halves  9272  nnrecl  9292  elnn0nn  9336  elnnnn0b  9338  elnnnn0c  9339  nn0addge1  9340  nn0addge2  9341  xnn0xrnemnf  9369  elnn0z  9384  elnnz1  9394  nzadd  9424  elz2  9443  zdivadd  9461  zdivmul  9462  zextle  9463  peano2uz2  9479  uzind  9483  btwnz  9491  uzss  9668  eluzp1m1  9671  infregelbex  9718  eluz2b2  9723  qre  9745  qaddcl  9755  qmulcl  9757  qreccl  9762  irradd  9766  irrmul  9767  elpqb  9770  cnref1o  9771  rprege0  9789  rprene0  9792  rpreap0  9793  rpcnne0  9794  rpcnap0  9795  rpregt0d  9824  rprege0d  9825  rprene0d  9826  rpcnne0d  9827  lediv2ad  9840  ledivge1le  9847  lediv12ad  9877  nnledivrp  9887  nn0ledivnn  9888  xrlttri3  9918  xrrebnd  9940  xrrege0  9946  xnn0xadd0  9988  xlesubadd  10004  elioo4g  10055  ioomax  10069  iccmax  10070  divelunit  10123  elfz5  10138  uzsubsubfz  10168  fzopth  10182  fzass4  10183  fzrev2  10206  uzsplit  10213  elfz2nn0  10233  difelfzle  10255  1fv  10260  4fvwrd4  10261  fzo1fzo0n0  10305  elfzom1elp1fzo  10329  subfzo0  10369  infssuzex  10374  qtri3or  10381  adddivflid  10433  flltdivnn0lt  10445  intfracq  10463  modqid2  10494  modfzo0difsn  10538  seq3val  10603  seqvalcd  10604  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemmo  10648  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seqf1oglem1  10662  seqf1oglem2  10663  expclzaplem  10706  leexp1a  10737  expubnd  10739  le2sq2  10758  sumsqeq0  10761  bernneq  10803  expnlbnd  10807  nn0opthd  10865  faclbnd6  10887  facavg  10889  seq3coll  10985  hash2en  10986  wrdnval  11022  ccat0  11050  ccatsymb  11056  shftlem  11069  shftfvalg  11071  shftfval  11074  cvg1nlemcau  11237  cvg1nlemres  11238  rexuz3  11243  resqrexlemcvg  11272  resqrexlemglsq  11275  resqrexlemga  11276  sqrtle  11289  sqrtlt  11290  sqrt11  11292  sqrtsq2  11296  absmul  11322  sqabs  11335  abslt  11341  absle  11342  lenegsq  11348  maxleastb  11467  maxltsup  11471  rexanre  11473  negfi  11481  xrmaxiflemab  11500  xrmaxiflemlub  11501  xrmaxltsup  11511  xrmaxadd  11514  climcn2  11562  mulcn2  11565  summodclem2a  11634  summodc  11636  fsum3  11640  fsum3cvg3  11649  fsumcl2lem  11651  fsumadd  11659  fsump1i  11686  fsum0diaglem  11693  mptfzshft  11695  fsumrev  11696  fsummulc2  11701  fsum00  11715  expcnvap0  11755  mertenslemi1  11788  ntrivcvgap0  11802  prodmodclem3  11828  prodmodclem2a  11829  zproddc  11832  fprodseq  11836  fprodrev  11872  fprodconst  11873  eftlub  11943  efieq  11988  sincos1sgn  12018  demoivreALT  12027  dvdsval3  12044  dvdscmul  12071  dvdsmulc  12072  dvdscmulr  12073  dvdsmulcr  12074  modmulconst  12076  dvds2ln  12077  ltoddhalfle  12146  nn0o  12160  divalg2  12179  ndvdssub  12183  ndvdsadd  12184  divgcdz  12234  gcd0id  12242  gcdaddm  12247  bezoutlemstep  12260  bezoutlemmain  12261  dfgcd3  12273  dfgcd2  12277  lcmcllem  12331  dvdslcm  12333  lcmgcdlem  12341  lcmgcdnn  12346  qredeq  12360  qredeu  12361  rpdvds  12363  divgcdcoprm0  12365  cncongr1  12367  cncongr2  12368  cncongrcoprm  12370  prmind2  12384  isprm5  12406  isprm6  12411  prmexpb  12415  cncongrprm  12421  sqrt2irrlem  12425  pw2dvdslemn  12429  oddpwdclemxy  12433  oddpwdclemdc  12437  oddpwdc  12438  hashdvds  12485  prmdiv  12499  hashgcdlem  12502  nnoddn2prmb  12527  pythagtriplem6  12535  pythagtriplem7  12536  pcpre1  12557  pccl  12564  pcmul  12566  pcdiv  12567  pcqmul  12568  pcqcl  12571  pcdvds  12580  pcndvds  12582  pcndvds2  12584  pc2dvds  12595  dvdsprmpweqle  12602  difsqpwdvds  12603  pcaddlem  12604  pcadd  12605  pcmptcl  12607  pcmpt  12608  fldivp1  12613  pcfac  12615  oddprmdvds  12619  infpnlem2  12625  4sqlem5  12647  4sqlem6  12648  4sqlem4a  12656  4sqexercise1  12663  4sqexercise2  12664  4sqlem13m  12668  4sqlem15  12670  4sqlem16  12671  ennnfonelemfun  12730  ennnfonelemim  12737  ctinfomlemom  12740  ctinfom  12741  ctinf  12743  ctiunctlemfo  12752  omctfn  12756  fnpr2ob  13114  ismgmid2  13154  fngsum  13162  igsumvalx  13163  gsumfzval  13165  gsum0g  13170  gsumval2  13171  issgrpd  13186  ismndd  13211  prdsidlem  13221  imasmnd2  13226  mhmf1o  13244  subsubm  13257  dfgrp2  13301  isgrpid2  13314  isgrpinv  13328  grplrinv  13331  dfgrp3mlem  13372  dfgrp3m  13373  dfgrp3me  13374  prdsinvlem  13382  imasgrp2  13388  mhmmnd  13394  issubg2m  13467  issubgrpd2  13468  grpissubg  13472  subsubg  13475  subgintm  13476  isnsg3  13485  nmzsubg  13488  eqgval  13501  eqgen  13505  isghmd  13530  ghmrn  13535  ghmpreima  13544  ghmf1o  13553  conjghm  13554  conjnmzb  13558  ghmpropd  13561  rinvmod  13587  imasabl  13614  rnglz  13649  isrngd  13657  srgdilem  13673  srglmhm  13697  srgrmhm  13698  ringdilem  13716  isringd  13745  ringsrg  13751  ringinvnzdiv  13754  imasring  13768  dvdsrd  13798  unitgrp  13820  isrim0  13865  isrhm2d  13869  rhmf1o  13872  rhmco  13878  rhmopp  13880  issubrng2  13914  subsubrng  13918  subrgugrp  13944  issubrg2  13945  subsubrg  13949  resrhm  13952  aprap  13990  lmodfopnelem2  14029  lsssubg  14081  islss3  14083  islss4  14086  lspsnel6  14112  lidlacl  14188  lidlsubg  14190  lidlrsppropdg  14199  2idlelbas  14220  cnfld1  14276  cnsubglem  14283  mulgghm2  14312  zndvds  14353  mplsubgfi  14405  topgele  14443  tgcl  14478  epttop  14504  opnssneib  14570  iscnp4  14632  cnco  14635  cncnp  14644  cnrest2  14650  lmss  14660  txcnp  14685  txcn  14689  cnmpt12  14701  cnmpt22  14708  hmeof1o  14723  psmetres2  14747  distspace  14749  ismeti  14760  isxmetd  14761  xmetpsmet  14783  xblss2ps  14818  xblss2  14819  blcntrps  14829  blcntr  14830  blin2  14846  mopni3  14898  metequiv2  14910  bdmet  14916  xmettx  14924  cnbl0  14948  cnblcld  14949  tgioo  14968  elcncf1di  14993  dedekindeulemlu  15035  suplociccex  15039  dedekindicclemlu  15044  dedekindicc  15047  ivthinclemlopn  15050  ivthdec  15058  ivthreinc  15059  ivthdichlem  15065  cnplimcim  15081  limccnp2lem  15090  dvfvalap  15095  plymullem  15164  reeff1olem  15185  sin0pilem1  15195  pilem3  15197  ptolemy  15238  sincosq1sgn  15240  sinq12gt0  15244  ioocosf1o  15268  rprelogbmulexp  15370  perfectlem2  15414  lgslem3  15421  lgsne0  15457  gausslemma2dlem0b  15469  gausslemma2dlem0c  15470  lgsquadlem2  15497  lgsquad2lem2  15501  2lgsoddprmlem2  15525  2sqlem8  15542  gropd  15586  grstructd2dom  15587  bj-nnan  15605  bj-charfun  15676  bdop  15744  bdunexb  15789  bj-om  15806  findset  15814  bj-peano4  15824  bj-inf2vn  15843  bj-inf2vn2  15844  pwle2  15868  pwf1oexmid  15869  nnnninfex  15892  sbthom  15898  qdencn  15899  trilpolemlt1  15913