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  1360  19.26  1495  nfand  1582  19.40  1645  equsexd  1743  sbcof2  1824  sbequ8  1861  eu2  2089  eu3h  2090  eu5  2092  mooran2  2118  datisi  2155  felapton  2159  darapti  2160  dimatis  2162  fresison  2163  fesapo  2165  reximssdv  2601  r19.26  2623  r19.29af2  2637  r19.40  2651  eqvinc  2887  eqvincg  2888  elrabd  2922  reu6  2953  reu3  2954  indifdir  3420  undif3ss  3425  un00  3498  eqifdc  3597  disjpr2  3687  prel12  3802  prneimg  3805  preqsn  3806  disjiun  4029  opth  4271  0nelop  4282  euotd  4288  opelopabsb  4295  ispod  4340  elon2  4412  unexb  4478  opeluu  4486  eusvnfb  4490  suc11g  4594  nlimsucg  4603  tfi  4619  vtoclr  4712  opthprc  4715  ideqg  4818  resiexg  4992  dminss  5085  imainss  5086  ssxpbm  5106  relrelss  5197  funopg  5293  fntpg  5315  fun11uni  5329  imain  5341  funimaexglem  5342  funssxp  5428  ffdm  5429  f00  5450  dffo2  5485  fodmrnu  5489  foco  5492  fun11iun  5526  f1o00  5540  fsnd  5548  fv3  5582  dff2  5707  dff3im  5708  dffo4  5711  ffnfv  5721  ffvresb  5726  fsn2  5737  fconstfvm  5781  fnfvima  5798  fcof1o  5837  isocnv  5859  isotr  5864  riotaprop  5902  acexmidlemcase  5918  caovlem2d  6118  f1ocnvd  6127  caofcom  6163  resfunexgALT  6167  elxp7  6230  2ndrn  6243  1stconst  6281  2ndconst  6282  cnvf1olem  6284  poxp  6292  dftpos4  6323  dfsmo2  6347  tfrlem5  6374  tfrlemiex  6391  tfr1onlemsucaccv  6401  tfr1onlembfn  6404  tfr1onlemex  6407  tfr1onlemres  6409  tfrcllemsucaccv  6414  tfrcllembfn  6417  tfrcllemex  6420  tfrcllemres  6422  tfrcl  6424  frecabex  6458  frecabcl  6459  frecfcllem  6464  frecrdg  6468  oawordi  6529  nntri3  6557  nntr2  6563  nnmordi  6576  iserd  6620  relelec  6636  erth  6640  qliftfun  6678  mapsncnv  6756  mptelixpg  6795  bren  6808  pw2f1odclem  6897  findcard2d  6954  findcard2sd  6955  isinfinf  6960  tridc  6962  nnwetri  6979  undifdcss  6986  fiintim  6994  fisseneq  6997  fidcenumlemim  7020  sbthlemi9  7033  supisolem  7076  ordiso2  7103  updjud  7150  difinfsn  7168  ctssdccl  7179  nnnninfeq  7196  omniwomnimkv  7235  acfun  7277  exmidontriimlem2  7292  onntri45  7311  dftap2  7321  netap  7324  2omotaplemap  7327  ccfunen  7334  cc4f  7339  cc4n  7341  elni2  7384  dfplpq2  7424  dfmpq2  7425  enqbreq2  7427  enqdc1  7432  addcmpblnq  7437  addclnq  7445  nqpi  7448  addassnqg  7452  mulassnqg  7454  mulcanenq  7455  distrnqg  7457  1qec  7458  recexnq  7460  subhalfnqq  7484  enq0tr  7504  nqnq0pi  7508  nq0nn  7512  mulcanenq0ec  7515  nnnq0lem1  7516  addclnq0  7521  distrnq0  7529  addassnq0lemcl  7531  elnp1st2nd  7546  prarloc  7573  addlocprlemlt  7601  addlocprlemeq  7603  addlocprlemgt  7604  addclpr  7607  nqprm  7612  mullocprlem  7640  mullocpr  7641  mulclpr  7642  ltpopr  7665  ltaddpr  7667  ltexprlemm  7670  ltexprlemopl  7671  ltexprlemopu  7673  ltexprlemrnd  7675  ltexprlemdisj  7676  addcanprleml  7684  addcanprlemu  7685  addcanprg  7686  recexprlemm  7694  recexprlemopl  7695  recexprlemopu  7697  recexprlemrnd  7699  recexprlemdisj  7700  cauappcvgprlemm  7715  cauappcvgprlemopl  7716  cauappcvgprlemopu  7718  cauappcvgprlemrnd  7720  cauappcvgprlemdisj  7721  cauappcvgprlemlim  7731  caucvgprlemnkj  7736  caucvgprlemm  7738  caucvgprlemopl  7739  caucvgprlemopu  7741  caucvgprlemrnd  7743  caucvgprlemlim  7751  caucvgprprlemnkltj  7759  caucvgprprlemnkeqj  7760  caucvgprprlemnjltk  7761  caucvgprprlemm  7766  caucvgprprlemopl  7767  caucvgprprlemopu  7769  caucvgprprlemrnd  7771  caucvgprprlemexbt  7776  caucvgprprlemlim  7781  suplocexprlemrl  7787  suplocexprlemru  7789  suplocexprlemdisj  7790  suplocexprlemloc  7791  suplocexprlemex  7792  suplocexprlemub  7793  prsrlem1  7812  mulclsr  7824  mulasssrg  7828  distrsrg  7829  suplocsrlemb  7876  elreal2  7900  axmulass  7943  axdistr  7944  axcaucvglemcau  7968  add20  8504  mullt0  8510  rereim  8616  ltmul1  8622  cru  8632  mulap0r  8645  aprcl  8676  aptap  8680  divmuldivap  8742  divmuleqap  8747  divadddivap  8757  divmuldivapd  8862  divmuleqapd  8863  div2subap  8867  ltmul12a  8890  lemul12a  8892  lemulge11  8896  lediv12a  8924  lediv2a  8925  recgt1i  8928  recreclt  8930  ledivp1  8933  lemul1ad  8969  lemul2ad  8970  ltmul12ad  8971  lemul12ad  8972  lemul12bd  8973  nndivre  9029  nndivtr  9035  halfaddsubcl  9227  halfaddsub  9228  lt2halves  9230  nnrecl  9250  elnn0nn  9294  elnnnn0b  9296  elnnnn0c  9297  nn0addge1  9298  nn0addge2  9299  xnn0xrnemnf  9327  elnn0z  9342  elnnz1  9352  nzadd  9381  elz2  9400  zdivadd  9418  zdivmul  9419  zextle  9420  peano2uz2  9436  uzind  9440  btwnz  9448  uzss  9625  eluzp1m1  9628  infregelbex  9675  eluz2b2  9680  qre  9702  qaddcl  9712  qmulcl  9714  qreccl  9719  irradd  9723  irrmul  9724  elpqb  9727  cnref1o  9728  rprege0  9746  rprene0  9749  rpreap0  9750  rpcnne0  9751  rpcnap0  9752  rpregt0d  9781  rprege0d  9782  rprene0d  9783  rpcnne0d  9784  lediv2ad  9797  ledivge1le  9804  lediv12ad  9834  nnledivrp  9844  nn0ledivnn  9845  xrlttri3  9875  xrrebnd  9897  xrrege0  9903  xnn0xadd0  9945  xlesubadd  9961  elioo4g  10012  ioomax  10026  iccmax  10027  divelunit  10080  elfz5  10095  uzsubsubfz  10125  fzopth  10139  fzass4  10140  fzrev2  10163  uzsplit  10170  elfz2nn0  10190  difelfzle  10212  1fv  10217  4fvwrd4  10218  fzo1fzo0n0  10262  elfzom1elp1fzo  10281  subfzo0  10321  infssuzex  10326  qtri3or  10333  adddivflid  10385  flltdivnn0lt  10397  intfracq  10415  modqid2  10446  modfzo0difsn  10490  seq3val  10555  seqvalcd  10556  iseqf1olemqcl  10594  iseqf1olemnab  10596  iseqf1olemab  10597  iseqf1olemmo  10600  seq3f1olemqsumkj  10606  seq3f1olemqsumk  10607  seqf1oglem1  10614  seqf1oglem2  10615  expclzaplem  10658  leexp1a  10689  expubnd  10691  le2sq2  10710  sumsqeq0  10713  bernneq  10755  expnlbnd  10759  nn0opthd  10817  faclbnd6  10839  facavg  10841  seq3coll  10937  wrdnval  10968  shftlem  10984  shftfvalg  10986  shftfval  10989  cvg1nlemcau  11152  cvg1nlemres  11153  rexuz3  11158  resqrexlemcvg  11187  resqrexlemglsq  11190  resqrexlemga  11191  sqrtle  11204  sqrtlt  11205  sqrt11  11207  sqrtsq2  11211  absmul  11237  sqabs  11250  abslt  11256  absle  11257  lenegsq  11263  maxleastb  11382  maxltsup  11386  rexanre  11388  negfi  11396  xrmaxiflemab  11415  xrmaxiflemlub  11416  xrmaxltsup  11426  xrmaxadd  11429  climcn2  11477  mulcn2  11480  summodclem2a  11549  summodc  11551  fsum3  11555  fsum3cvg3  11564  fsumcl2lem  11566  fsumadd  11574  fsump1i  11601  fsum0diaglem  11608  mptfzshft  11610  fsumrev  11611  fsummulc2  11616  fsum00  11630  expcnvap0  11670  mertenslemi1  11703  ntrivcvgap0  11717  prodmodclem3  11743  prodmodclem2a  11744  zproddc  11747  fprodseq  11751  fprodrev  11787  fprodconst  11788  eftlub  11858  efieq  11903  sincos1sgn  11933  demoivreALT  11942  dvdsval3  11959  dvdscmul  11986  dvdsmulc  11987  dvdscmulr  11988  dvdsmulcr  11989  modmulconst  11991  dvds2ln  11992  ltoddhalfle  12061  nn0o  12075  divalg2  12094  ndvdssub  12098  ndvdsadd  12099  divgcdz  12149  gcd0id  12157  gcdaddm  12162  bezoutlemstep  12175  bezoutlemmain  12176  dfgcd3  12188  dfgcd2  12192  lcmcllem  12246  dvdslcm  12248  lcmgcdlem  12256  lcmgcdnn  12261  qredeq  12275  qredeu  12276  rpdvds  12278  divgcdcoprm0  12280  cncongr1  12282  cncongr2  12283  cncongrcoprm  12285  prmind2  12299  isprm5  12321  isprm6  12326  prmexpb  12330  cncongrprm  12336  sqrt2irrlem  12340  pw2dvdslemn  12344  oddpwdclemxy  12348  oddpwdclemdc  12352  oddpwdc  12353  hashdvds  12400  prmdiv  12414  hashgcdlem  12417  nnoddn2prmb  12442  pythagtriplem6  12450  pythagtriplem7  12451  pcpre1  12472  pccl  12479  pcmul  12481  pcdiv  12482  pcqmul  12483  pcqcl  12486  pcdvds  12495  pcndvds  12497  pcndvds2  12499  pc2dvds  12510  dvdsprmpweqle  12517  difsqpwdvds  12518  pcaddlem  12519  pcadd  12520  pcmptcl  12522  pcmpt  12523  fldivp1  12528  pcfac  12530  oddprmdvds  12534  infpnlem2  12540  4sqlem5  12562  4sqlem6  12563  4sqlem4a  12571  4sqexercise1  12578  4sqexercise2  12579  4sqlem13m  12583  4sqlem15  12585  4sqlem16  12586  ennnfonelemfun  12645  ennnfonelemim  12652  ctinfomlemom  12655  ctinfom  12656  ctinf  12658  ctiunctlemfo  12667  omctfn  12671  fnpr2ob  13009  ismgmid2  13049  fngsum  13057  igsumvalx  13058  gsumfzval  13060  gsum0g  13065  gsumval2  13066  issgrpd  13081  ismndd  13104  mhmf1o  13128  subsubm  13141  dfgrp2  13185  isgrpid2  13198  isgrpinv  13212  grplrinv  13215  dfgrp3mlem  13256  dfgrp3m  13257  dfgrp3me  13258  imasgrp2  13266  mhmmnd  13272  issubg2m  13345  issubgrpd2  13346  grpissubg  13350  subsubg  13353  subgintm  13354  isnsg3  13363  nmzsubg  13366  eqgval  13379  eqgen  13383  isghmd  13408  ghmrn  13413  ghmpreima  13422  ghmf1o  13431  conjghm  13432  conjnmzb  13436  ghmpropd  13439  rinvmod  13465  imasabl  13492  rnglz  13527  isrngd  13535  srgdilem  13551  srglmhm  13575  srgrmhm  13576  ringdilem  13594  isringd  13623  ringsrg  13629  ringinvnzdiv  13632  imasring  13646  dvdsrd  13676  unitgrp  13698  isrim0  13743  isrhm2d  13747  rhmf1o  13750  rhmco  13756  rhmopp  13758  issubrng2  13792  subsubrng  13796  subrgugrp  13822  issubrg2  13823  subsubrg  13827  resrhm  13830  aprap  13868  lmodfopnelem2  13907  lsssubg  13959  islss3  13961  islss4  13964  lspsnel6  13990  lidlacl  14066  lidlsubg  14068  lidlrsppropdg  14077  2idlelbas  14098  cnfld1  14154  cnsubglem  14161  mulgghm2  14190  zndvds  14231  topgele  14291  tgcl  14326  epttop  14352  opnssneib  14418  iscnp4  14480  cnco  14483  cncnp  14492  cnrest2  14498  lmss  14508  txcnp  14533  txcn  14537  cnmpt12  14549  cnmpt22  14556  hmeof1o  14571  psmetres2  14595  distspace  14597  ismeti  14608  isxmetd  14609  xmetpsmet  14631  xblss2ps  14666  xblss2  14667  blcntrps  14677  blcntr  14678  blin2  14694  mopni3  14746  metequiv2  14758  bdmet  14764  xmettx  14772  cnbl0  14796  cnblcld  14797  tgioo  14816  elcncf1di  14841  dedekindeulemlu  14883  suplociccex  14887  dedekindicclemlu  14892  dedekindicc  14895  ivthinclemlopn  14898  ivthdec  14906  ivthreinc  14907  ivthdichlem  14913  cnplimcim  14929  limccnp2lem  14938  dvfvalap  14943  plymullem  15012  reeff1olem  15033  sin0pilem1  15043  pilem3  15045  ptolemy  15086  sincosq1sgn  15088  sinq12gt0  15092  ioocosf1o  15116  rprelogbmulexp  15218  perfectlem2  15262  lgslem3  15269  lgsne0  15305  gausslemma2dlem0b  15317  gausslemma2dlem0c  15318  lgsquadlem2  15345  lgsquad2lem2  15349  2lgsoddprmlem2  15373  2sqlem8  15390  bj-nnan  15408  bj-charfun  15479  bdop  15547  bdunexb  15592  bj-om  15609  findset  15617  bj-peano4  15627  bj-inf2vn  15646  bj-inf2vn2  15647  pwle2  15671  pwf1oexmid  15672  sbthom  15699  qdencn  15700  trilpolemlt1  15714