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  2926  eqvincg  2927  elrabd  2961  reu6  2992  reu3  2993  indifdir  3460  undif3ss  3465  un00  3538  eqifdc  3639  disjpr2  3730  prel12  3849  prneimg  3852  preqsn  3853  disjiun  4078  opth  4323  0nelop  4334  euotd  4341  opelopabsb  4348  ispod  4395  elon2  4467  unexb  4533  opeluu  4541  eusvnfb  4545  suc11g  4649  nlimsucg  4658  tfi  4674  vtoclr  4767  opthprc  4770  ideqg  4873  resiexg  5050  dminss  5143  imainss  5144  ssxpbm  5164  relrelss  5255  funopg  5352  fununfun  5364  fntpg  5377  fun11uni  5391  imain  5403  funimaexglem  5404  funssxp  5495  ffdm  5496  f00  5519  dffo2  5554  fodmrnu  5558  foco  5561  fun11iun  5595  f1o00  5610  fsnd  5618  fv3  5652  dff2  5781  dff3im  5782  dffo4  5785  ffnfv  5795  ffvresb  5800  fsn2  5811  fconstfvm  5861  fnfvima  5878  resfvresima  5880  fcof1o  5919  isocnv  5941  isotr  5946  riotaprop  5986  acexmidlemcase  6002  caovlem2d  6204  f1ocnvd  6214  caofcom  6255  resfunexgALT  6259  elxp7  6322  2ndrn  6335  1stconst  6373  2ndconst  6374  cnvf1olem  6376  poxp  6384  dftpos4  6415  dfsmo2  6439  tfrlem5  6466  tfrlemiex  6483  tfr1onlemsucaccv  6493  tfr1onlembfn  6496  tfr1onlemex  6499  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembfn  6509  tfrcllemex  6512  tfrcllemres  6514  tfrcl  6516  frecabex  6550  frecabcl  6551  frecfcllem  6556  frecrdg  6560  oawordi  6623  nntri3  6651  nntr2  6657  nnmordi  6670  iserd  6714  relelec  6730  erth  6734  qliftfun  6772  mapsncnv  6850  mptelixpg  6889  bren  6903  pw2f1odclem  7003  findcard2d  7061  findcard2sd  7062  isinfinf  7067  tridc  7070  nnwetri  7089  undifdcss  7096  fiintim  7104  fisseneq  7107  fidcenumlemim  7130  sbthlemi9  7143  supisolem  7186  ordiso2  7213  updjud  7260  difinfsn  7278  ctssdccl  7289  nnnninfeq  7306  omniwomnimkv  7345  pr2cv  7381  acfun  7400  exmidontriimlem2  7415  onntri45  7437  dftap2  7448  netap  7451  2omotaplemap  7454  ccfunen  7461  cc4f  7466  cc4n  7468  elni2  7512  dfplpq2  7552  dfmpq2  7553  enqbreq2  7555  enqdc1  7560  addcmpblnq  7565  addclnq  7573  nqpi  7576  addassnqg  7580  mulassnqg  7582  mulcanenq  7583  distrnqg  7585  1qec  7586  recexnq  7588  subhalfnqq  7612  enq0tr  7632  nqnq0pi  7636  nq0nn  7640  mulcanenq0ec  7643  nnnq0lem1  7644  addclnq0  7649  distrnq0  7657  addassnq0lemcl  7659  elnp1st2nd  7674  prarloc  7701  addlocprlemlt  7729  addlocprlemeq  7731  addlocprlemgt  7732  addclpr  7735  nqprm  7740  mullocprlem  7768  mullocpr  7769  mulclpr  7770  ltpopr  7793  ltaddpr  7795  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemrnd  7803  ltexprlemdisj  7804  addcanprleml  7812  addcanprlemu  7813  addcanprg  7814  recexprlemm  7822  recexprlemopl  7823  recexprlemopu  7825  recexprlemrnd  7827  recexprlemdisj  7828  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemrnd  7848  cauappcvgprlemdisj  7849  cauappcvgprlemlim  7859  caucvgprlemnkj  7864  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemrnd  7871  caucvgprlemlim  7879  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  caucvgprprlemm  7894  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemrnd  7899  caucvgprprlemexbt  7904  caucvgprprlemlim  7909  suplocexprlemrl  7915  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  prsrlem1  7940  mulclsr  7952  mulasssrg  7956  distrsrg  7957  suplocsrlemb  8004  elreal2  8028  axmulass  8071  axdistr  8072  axcaucvglemcau  8096  add20  8632  mullt0  8638  rereim  8744  ltmul1  8750  cru  8760  mulap0r  8773  aprcl  8804  aptap  8808  divmuldivap  8870  divmuleqap  8875  divadddivap  8885  divmuldivapd  8990  divmuleqapd  8991  div2subap  8995  ltmul12a  9018  lemul12a  9020  lemulge11  9024  lediv12a  9052  lediv2a  9053  recgt1i  9056  recreclt  9058  ledivp1  9061  lemul1ad  9097  lemul2ad  9098  ltmul12ad  9099  lemul12ad  9100  lemul12bd  9101  nndivre  9157  nndivtr  9163  halfaddsubcl  9355  halfaddsub  9356  lt2halves  9358  nnrecl  9378  elnn0nn  9422  elnnnn0b  9424  elnnnn0c  9425  nn0addge1  9426  nn0addge2  9427  xnn0xrnemnf  9455  elnn0z  9470  elnnz1  9480  nzadd  9510  elz2  9529  zdivadd  9547  zdivmul  9548  zextle  9549  peano2uz2  9565  uzind  9569  btwnz  9577  uzss  9755  eluzp1m1  9758  infregelbex  9805  eluz2b2  9810  qre  9832  qaddcl  9842  qmulcl  9844  qreccl  9849  irradd  9853  irrmul  9854  elpqb  9857  cnref1o  9858  rprege0  9876  rprene0  9879  rpreap0  9880  rpcnne0  9881  rpcnap0  9882  rpregt0d  9911  rprege0d  9912  rprene0d  9913  rpcnne0d  9914  lediv2ad  9927  ledivge1le  9934  lediv12ad  9964  nnledivrp  9974  nn0ledivnn  9975  xrlttri3  10005  xrrebnd  10027  xrrege0  10033  xnn0xadd0  10075  xlesubadd  10091  elioo4g  10142  ioomax  10156  iccmax  10157  divelunit  10210  elfz5  10225  uzsubsubfz  10255  fzopth  10269  fzass4  10270  fzrev2  10293  uzsplit  10300  elfz2nn0  10320  difelfzle  10342  1fv  10347  4fvwrd4  10348  fzo1fzo0n0  10395  elfzom1elp1fzo  10420  subfzo0  10460  infssuzex  10465  qtri3or  10472  adddivflid  10524  flltdivnn0lt  10536  intfracq  10554  modqid2  10585  modfzo0difsn  10629  seq3val  10694  seqvalcd  10695  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemmo  10739  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seqf1oglem1  10753  seqf1oglem2  10754  expclzaplem  10797  leexp1a  10828  expubnd  10830  le2sq2  10849  sumsqeq0  10852  bernneq  10894  expnlbnd  10898  nn0opthd  10956  faclbnd6  10978  facavg  10980  seq3coll  11077  hash2en  11078  wrdnval  11115  ccat0  11144  ccatsymb  11150  ccatalpha  11161  swrdspsleq  11214  pfxtrcfv  11240  pfxsuffeqwrdeq  11245  wrd2ind  11270  pfxccatin12lem2a  11274  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  pfxccatpfx1  11283  pfxccatpfx2  11284  swrdccatin1d  11290  swrdccatin2d  11291  shftlem  11342  shftfvalg  11344  shftfval  11347  cvg1nlemcau  11510  cvg1nlemres  11511  rexuz3  11516  resqrexlemcvg  11545  resqrexlemglsq  11548  resqrexlemga  11549  sqrtle  11562  sqrtlt  11563  sqrt11  11565  sqrtsq2  11569  absmul  11595  sqabs  11608  abslt  11614  absle  11615  lenegsq  11621  maxleastb  11740  maxltsup  11744  rexanre  11746  negfi  11754  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxltsup  11784  xrmaxadd  11787  climcn2  11835  mulcn2  11838  summodclem2a  11907  summodc  11909  fsum3  11913  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  fsump1i  11959  fsum0diaglem  11966  mptfzshft  11968  fsumrev  11969  fsummulc2  11974  fsum00  11988  expcnvap0  12028  mertenslemi1  12061  ntrivcvgap0  12075  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodrev  12145  fprodconst  12146  eftlub  12216  efieq  12261  sincos1sgn  12291  demoivreALT  12300  dvdsval3  12317  dvdscmul  12344  dvdsmulc  12345  dvdscmulr  12346  dvdsmulcr  12347  modmulconst  12349  dvds2ln  12350  ltoddhalfle  12419  nn0o  12433  divalg2  12452  ndvdssub  12456  ndvdsadd  12457  divgcdz  12507  gcd0id  12515  gcdaddm  12520  bezoutlemstep  12533  bezoutlemmain  12534  dfgcd3  12546  dfgcd2  12550  lcmcllem  12604  dvdslcm  12606  lcmgcdlem  12614  lcmgcdnn  12619  qredeq  12633  qredeu  12634  rpdvds  12636  divgcdcoprm0  12638  cncongr1  12640  cncongr2  12641  cncongrcoprm  12643  prmind2  12657  isprm5  12679  isprm6  12684  prmexpb  12688  cncongrprm  12694  sqrt2irrlem  12698  pw2dvdslemn  12702  oddpwdclemxy  12706  oddpwdclemdc  12710  oddpwdc  12711  hashdvds  12758  prmdiv  12772  hashgcdlem  12775  nnoddn2prmb  12800  pythagtriplem6  12808  pythagtriplem7  12809  pcpre1  12830  pccl  12837  pcmul  12839  pcdiv  12840  pcqmul  12841  pcqcl  12844  pcdvds  12853  pcndvds  12855  pcndvds2  12857  pc2dvds  12868  dvdsprmpweqle  12875  difsqpwdvds  12876  pcaddlem  12877  pcadd  12878  pcmptcl  12880  pcmpt  12881  fldivp1  12886  pcfac  12888  oddprmdvds  12892  infpnlem2  12898  4sqlem5  12920  4sqlem6  12921  4sqlem4a  12929  4sqexercise1  12936  4sqexercise2  12937  4sqlem13m  12941  4sqlem15  12943  4sqlem16  12944  ennnfonelemfun  13003  ennnfonelemim  13010  ctinfomlemom  13013  ctinfom  13014  ctinf  13016  ctiunctlemfo  13025  omctfn  13029  fnpr2ob  13388  ismgmid2  13428  fngsum  13436  igsumvalx  13437  gsumfzval  13439  gsum0g  13444  gsumval2  13445  issgrpd  13460  ismndd  13485  prdsidlem  13495  imasmnd2  13500  mhmf1o  13518  subsubm  13531  dfgrp2  13575  isgrpid2  13588  isgrpinv  13602  grplrinv  13605  dfgrp3mlem  13646  dfgrp3m  13647  dfgrp3me  13648  prdsinvlem  13656  imasgrp2  13662  mhmmnd  13668  issubg2m  13741  issubgrpd2  13742  grpissubg  13746  subsubg  13749  subgintm  13750  isnsg3  13759  nmzsubg  13762  eqgval  13775  eqgen  13779  isghmd  13804  ghmrn  13809  ghmpreima  13818  ghmf1o  13827  conjghm  13828  conjnmzb  13832  ghmpropd  13835  rinvmod  13861  imasabl  13888  rnglz  13923  isrngd  13931  srgdilem  13947  srglmhm  13971  srgrmhm  13972  ringdilem  13990  isringd  14019  ringsrg  14025  ringinvnzdiv  14028  imasring  14042  dvdsrd  14073  unitgrp  14095  isrim0  14140  isrhm2d  14144  rhmf1o  14147  rhmco  14153  rhmopp  14155  issubrng2  14189  subsubrng  14193  subrgugrp  14219  issubrg2  14220  subsubrg  14224  resrhm  14227  aprap  14265  lmodfopnelem2  14304  lsssubg  14356  islss3  14358  islss4  14361  lspsnel6  14387  lidlacl  14463  lidlsubg  14465  lidlrsppropdg  14474  2idlelbas  14495  cnfld1  14551  cnsubglem  14558  mulgghm2  14587  zndvds  14628  mplsubgfi  14680  topgele  14718  tgcl  14753  epttop  14779  opnssneib  14845  iscnp4  14907  cnco  14910  cncnp  14919  cnrest2  14925  lmss  14935  txcnp  14960  txcn  14964  cnmpt12  14976  cnmpt22  14983  hmeof1o  14998  psmetres2  15022  distspace  15024  ismeti  15035  isxmetd  15036  xmetpsmet  15058  xblss2ps  15093  xblss2  15094  blcntrps  15104  blcntr  15105  blin2  15121  mopni3  15173  metequiv2  15185  bdmet  15191  xmettx  15199  cnbl0  15223  cnblcld  15224  tgioo  15243  elcncf1di  15268  dedekindeulemlu  15310  suplociccex  15314  dedekindicclemlu  15319  dedekindicc  15322  ivthinclemlopn  15325  ivthdec  15333  ivthreinc  15334  ivthdichlem  15340  cnplimcim  15356  limccnp2lem  15365  dvfvalap  15370  plymullem  15439  reeff1olem  15460  sin0pilem1  15470  pilem3  15472  ptolemy  15513  sincosq1sgn  15515  sinq12gt0  15519  ioocosf1o  15543  rprelogbmulexp  15645  perfectlem2  15689  lgslem3  15696  lgsne0  15732  gausslemma2dlem0b  15744  gausslemma2dlem0c  15745  lgsquadlem2  15772  lgsquad2lem2  15776  2lgsoddprmlem2  15800  2sqlem8  15817  gropd  15863  grstructd2dom  15864  incistruhgr  15905  umgrislfupgrenlem  15943  umgrislfupgrdom  15944  uspgrupgrushgr  15995  usgrumgruspgr  15998  usgruspgrben  15999  usgrislfuspgrdom  16003  umgrvad2edg  16024  umgr2edgneu  16025  ushgredgedg  16039  ushgredgedgloop  16041  iswlkg  16070  wlk2f  16092  upgriswlkdc  16101  wlkv0  16110  wlklenvclwlk  16114  upgr2wlkdc  16116  wlkres  16118  clwwlkccatlem  16137  clwwlkccat  16138  bj-nnan  16155  bj-charfun  16225  bdop  16293  bdunexb  16338  bj-om  16355  findset  16363  bj-peano4  16373  bj-inf2vn  16392  bj-inf2vn2  16393  pwle2  16423  pwf1oexmid  16424  nnnninfex  16448  sbthom  16454  qdencn  16455  trilpolemlt1  16469