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  754  ordi  818  stdcndc  847  stdcndcOLD  848  dfandc  886  mpbi2and  946  mpbir2and  947  pm4.82  953  pm4.83dc  954  rnlem  979  syl22anc  1251  syl112anc  1254  syl121anc  1255  syl211anc  1256  syl23anc  1257  syl32anc  1258  syl122anc  1259  syl212anc  1260  syl221anc  1261  syl222anc  1266  syl123anc  1267  syl132anc  1268  syl213anc  1269  syl231anc  1270  syl312anc  1271  syl321anc  1272  syl223anc  1276  syl232anc  1277  syl322anc  1278  syl233anc  1279  syl323anc  1280  syl332anc  1281  ecased  1362  19.26  1504  nfand  1591  19.40  1654  equsexd  1752  sbcof2  1833  sbequ8  1870  eu2  2098  eu3h  2099  eu5  2101  mooran2  2127  datisi  2164  felapton  2168  darapti  2169  dimatis  2171  fresison  2172  fesapo  2174  reximssdv  2610  r19.26  2632  r19.29af2  2646  r19.40  2660  eqvinc  2896  eqvincg  2897  elrabd  2931  reu6  2962  reu3  2963  indifdir  3429  undif3ss  3434  un00  3507  eqifdc  3607  disjpr2  3697  prel12  3812  prneimg  3815  preqsn  3816  disjiun  4039  opth  4281  0nelop  4292  euotd  4299  opelopabsb  4306  ispod  4351  elon2  4423  unexb  4489  opeluu  4497  eusvnfb  4501  suc11g  4605  nlimsucg  4614  tfi  4630  vtoclr  4723  opthprc  4726  ideqg  4829  resiexg  5004  dminss  5097  imainss  5098  ssxpbm  5118  relrelss  5209  funopg  5305  fununfun  5317  fntpg  5330  fun11uni  5344  imain  5356  funimaexglem  5357  funssxp  5445  ffdm  5446  f00  5467  dffo2  5502  fodmrnu  5506  foco  5509  fun11iun  5543  f1o00  5557  fsnd  5565  fv3  5599  dff2  5724  dff3im  5725  dffo4  5728  ffnfv  5738  ffvresb  5743  fsn2  5754  fconstfvm  5802  fnfvima  5819  fcof1o  5858  isocnv  5880  isotr  5885  riotaprop  5923  acexmidlemcase  5939  caovlem2d  6139  f1ocnvd  6148  caofcom  6189  resfunexgALT  6193  elxp7  6256  2ndrn  6269  1stconst  6307  2ndconst  6308  cnvf1olem  6310  poxp  6318  dftpos4  6349  dfsmo2  6373  tfrlem5  6400  tfrlemiex  6417  tfr1onlemsucaccv  6427  tfr1onlembfn  6430  tfr1onlemex  6433  tfr1onlemres  6435  tfrcllemsucaccv  6440  tfrcllembfn  6443  tfrcllemex  6446  tfrcllemres  6448  tfrcl  6450  frecabex  6484  frecabcl  6485  frecfcllem  6490  frecrdg  6494  oawordi  6555  nntri3  6583  nntr2  6589  nnmordi  6602  iserd  6646  relelec  6662  erth  6666  qliftfun  6704  mapsncnv  6782  mptelixpg  6821  bren  6835  pw2f1odclem  6931  findcard2d  6988  findcard2sd  6989  isinfinf  6994  tridc  6996  nnwetri  7013  undifdcss  7020  fiintim  7028  fisseneq  7031  fidcenumlemim  7054  sbthlemi9  7067  supisolem  7110  ordiso2  7137  updjud  7184  difinfsn  7202  ctssdccl  7213  nnnninfeq  7230  omniwomnimkv  7269  acfun  7319  exmidontriimlem2  7334  onntri45  7353  dftap2  7363  netap  7366  2omotaplemap  7369  ccfunen  7376  cc4f  7381  cc4n  7383  elni2  7427  dfplpq2  7467  dfmpq2  7468  enqbreq2  7470  enqdc1  7475  addcmpblnq  7480  addclnq  7488  nqpi  7491  addassnqg  7495  mulassnqg  7497  mulcanenq  7498  distrnqg  7500  1qec  7501  recexnq  7503  subhalfnqq  7527  enq0tr  7547  nqnq0pi  7551  nq0nn  7555  mulcanenq0ec  7558  nnnq0lem1  7559  addclnq0  7564  distrnq0  7572  addassnq0lemcl  7574  elnp1st2nd  7589  prarloc  7616  addlocprlemlt  7644  addlocprlemeq  7646  addlocprlemgt  7647  addclpr  7650  nqprm  7655  mullocprlem  7683  mullocpr  7684  mulclpr  7685  ltpopr  7708  ltaddpr  7710  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemrnd  7718  ltexprlemdisj  7719  addcanprleml  7727  addcanprlemu  7728  addcanprg  7729  recexprlemm  7737  recexprlemopl  7738  recexprlemopu  7740  recexprlemrnd  7742  recexprlemdisj  7743  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemopu  7761  cauappcvgprlemrnd  7763  cauappcvgprlemdisj  7764  cauappcvgprlemlim  7774  caucvgprlemnkj  7779  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemopu  7784  caucvgprlemrnd  7786  caucvgprlemlim  7794  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnjltk  7804  caucvgprprlemm  7809  caucvgprprlemopl  7810  caucvgprprlemopu  7812  caucvgprprlemrnd  7814  caucvgprprlemexbt  7819  caucvgprprlemlim  7824  suplocexprlemrl  7830  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemex  7835  suplocexprlemub  7836  prsrlem1  7855  mulclsr  7867  mulasssrg  7871  distrsrg  7872  suplocsrlemb  7919  elreal2  7943  axmulass  7986  axdistr  7987  axcaucvglemcau  8011  add20  8547  mullt0  8553  rereim  8659  ltmul1  8665  cru  8675  mulap0r  8688  aprcl  8719  aptap  8723  divmuldivap  8785  divmuleqap  8790  divadddivap  8800  divmuldivapd  8905  divmuleqapd  8906  div2subap  8910  ltmul12a  8933  lemul12a  8935  lemulge11  8939  lediv12a  8967  lediv2a  8968  recgt1i  8971  recreclt  8973  ledivp1  8976  lemul1ad  9012  lemul2ad  9013  ltmul12ad  9014  lemul12ad  9015  lemul12bd  9016  nndivre  9072  nndivtr  9078  halfaddsubcl  9270  halfaddsub  9271  lt2halves  9273  nnrecl  9293  elnn0nn  9337  elnnnn0b  9339  elnnnn0c  9340  nn0addge1  9341  nn0addge2  9342  xnn0xrnemnf  9370  elnn0z  9385  elnnz1  9395  nzadd  9425  elz2  9444  zdivadd  9462  zdivmul  9463  zextle  9464  peano2uz2  9480  uzind  9484  btwnz  9492  uzss  9669  eluzp1m1  9672  infregelbex  9719  eluz2b2  9724  qre  9746  qaddcl  9756  qmulcl  9758  qreccl  9763  irradd  9767  irrmul  9768  elpqb  9771  cnref1o  9772  rprege0  9790  rprene0  9793  rpreap0  9794  rpcnne0  9795  rpcnap0  9796  rpregt0d  9825  rprege0d  9826  rprene0d  9827  rpcnne0d  9828  lediv2ad  9841  ledivge1le  9848  lediv12ad  9878  nnledivrp  9888  nn0ledivnn  9889  xrlttri3  9919  xrrebnd  9941  xrrege0  9947  xnn0xadd0  9989  xlesubadd  10005  elioo4g  10056  ioomax  10070  iccmax  10071  divelunit  10124  elfz5  10139  uzsubsubfz  10169  fzopth  10183  fzass4  10184  fzrev2  10207  uzsplit  10214  elfz2nn0  10234  difelfzle  10256  1fv  10261  4fvwrd4  10262  fzo1fzo0n0  10307  elfzom1elp1fzo  10331  subfzo0  10371  infssuzex  10376  qtri3or  10383  adddivflid  10435  flltdivnn0lt  10447  intfracq  10465  modqid2  10496  modfzo0difsn  10540  seq3val  10605  seqvalcd  10606  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemmo  10650  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seqf1oglem1  10664  seqf1oglem2  10665  expclzaplem  10708  leexp1a  10739  expubnd  10741  le2sq2  10760  sumsqeq0  10763  bernneq  10805  expnlbnd  10809  nn0opthd  10867  faclbnd6  10889  facavg  10891  seq3coll  10987  hash2en  10988  wrdnval  11024  ccat0  11052  ccatsymb  11058  swrdspsleq  11120  shftlem  11127  shftfvalg  11129  shftfval  11132  cvg1nlemcau  11295  cvg1nlemres  11296  rexuz3  11301  resqrexlemcvg  11330  resqrexlemglsq  11333  resqrexlemga  11334  sqrtle  11347  sqrtlt  11348  sqrt11  11350  sqrtsq2  11354  absmul  11380  sqabs  11393  abslt  11399  absle  11400  lenegsq  11406  maxleastb  11525  maxltsup  11529  rexanre  11531  negfi  11539  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxltsup  11569  xrmaxadd  11572  climcn2  11620  mulcn2  11623  summodclem2a  11692  summodc  11694  fsum3  11698  fsum3cvg3  11707  fsumcl2lem  11709  fsumadd  11717  fsump1i  11744  fsum0diaglem  11751  mptfzshft  11753  fsumrev  11754  fsummulc2  11759  fsum00  11773  expcnvap0  11813  mertenslemi1  11846  ntrivcvgap0  11860  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodrev  11930  fprodconst  11931  eftlub  12001  efieq  12046  sincos1sgn  12076  demoivreALT  12085  dvdsval3  12102  dvdscmul  12129  dvdsmulc  12130  dvdscmulr  12131  dvdsmulcr  12132  modmulconst  12134  dvds2ln  12135  ltoddhalfle  12204  nn0o  12218  divalg2  12237  ndvdssub  12241  ndvdsadd  12242  divgcdz  12292  gcd0id  12300  gcdaddm  12305  bezoutlemstep  12318  bezoutlemmain  12319  dfgcd3  12331  dfgcd2  12335  lcmcllem  12389  dvdslcm  12391  lcmgcdlem  12399  lcmgcdnn  12404  qredeq  12418  qredeu  12419  rpdvds  12421  divgcdcoprm0  12423  cncongr1  12425  cncongr2  12426  cncongrcoprm  12428  prmind2  12442  isprm5  12464  isprm6  12469  prmexpb  12473  cncongrprm  12479  sqrt2irrlem  12483  pw2dvdslemn  12487  oddpwdclemxy  12491  oddpwdclemdc  12495  oddpwdc  12496  hashdvds  12543  prmdiv  12557  hashgcdlem  12560  nnoddn2prmb  12585  pythagtriplem6  12593  pythagtriplem7  12594  pcpre1  12615  pccl  12622  pcmul  12624  pcdiv  12625  pcqmul  12626  pcqcl  12629  pcdvds  12638  pcndvds  12640  pcndvds2  12642  pc2dvds  12653  dvdsprmpweqle  12660  difsqpwdvds  12661  pcaddlem  12662  pcadd  12663  pcmptcl  12665  pcmpt  12666  fldivp1  12671  pcfac  12673  oddprmdvds  12677  infpnlem2  12683  4sqlem5  12705  4sqlem6  12706  4sqlem4a  12714  4sqexercise1  12721  4sqexercise2  12722  4sqlem13m  12726  4sqlem15  12728  4sqlem16  12729  ennnfonelemfun  12788  ennnfonelemim  12795  ctinfomlemom  12798  ctinfom  12799  ctinf  12801  ctiunctlemfo  12810  omctfn  12814  fnpr2ob  13172  ismgmid2  13212  fngsum  13220  igsumvalx  13221  gsumfzval  13223  gsum0g  13228  gsumval2  13229  issgrpd  13244  ismndd  13269  prdsidlem  13279  imasmnd2  13284  mhmf1o  13302  subsubm  13315  dfgrp2  13359  isgrpid2  13372  isgrpinv  13386  grplrinv  13389  dfgrp3mlem  13430  dfgrp3m  13431  dfgrp3me  13432  prdsinvlem  13440  imasgrp2  13446  mhmmnd  13452  issubg2m  13525  issubgrpd2  13526  grpissubg  13530  subsubg  13533  subgintm  13534  isnsg3  13543  nmzsubg  13546  eqgval  13559  eqgen  13563  isghmd  13588  ghmrn  13593  ghmpreima  13602  ghmf1o  13611  conjghm  13612  conjnmzb  13616  ghmpropd  13619  rinvmod  13645  imasabl  13672  rnglz  13707  isrngd  13715  srgdilem  13731  srglmhm  13755  srgrmhm  13756  ringdilem  13774  isringd  13803  ringsrg  13809  ringinvnzdiv  13812  imasring  13826  dvdsrd  13856  unitgrp  13878  isrim0  13923  isrhm2d  13927  rhmf1o  13930  rhmco  13936  rhmopp  13938  issubrng2  13972  subsubrng  13976  subrgugrp  14002  issubrg2  14003  subsubrg  14007  resrhm  14010  aprap  14048  lmodfopnelem2  14087  lsssubg  14139  islss3  14141  islss4  14144  lspsnel6  14170  lidlacl  14246  lidlsubg  14248  lidlrsppropdg  14257  2idlelbas  14278  cnfld1  14334  cnsubglem  14341  mulgghm2  14370  zndvds  14411  mplsubgfi  14463  topgele  14501  tgcl  14536  epttop  14562  opnssneib  14628  iscnp4  14690  cnco  14693  cncnp  14702  cnrest2  14708  lmss  14718  txcnp  14743  txcn  14747  cnmpt12  14759  cnmpt22  14766  hmeof1o  14781  psmetres2  14805  distspace  14807  ismeti  14818  isxmetd  14819  xmetpsmet  14841  xblss2ps  14876  xblss2  14877  blcntrps  14887  blcntr  14888  blin2  14904  mopni3  14956  metequiv2  14968  bdmet  14974  xmettx  14982  cnbl0  15006  cnblcld  15007  tgioo  15026  elcncf1di  15051  dedekindeulemlu  15093  suplociccex  15097  dedekindicclemlu  15102  dedekindicc  15105  ivthinclemlopn  15108  ivthdec  15116  ivthreinc  15117  ivthdichlem  15123  cnplimcim  15139  limccnp2lem  15148  dvfvalap  15153  plymullem  15222  reeff1olem  15243  sin0pilem1  15253  pilem3  15255  ptolemy  15296  sincosq1sgn  15298  sinq12gt0  15302  ioocosf1o  15326  rprelogbmulexp  15428  perfectlem2  15472  lgslem3  15479  lgsne0  15515  gausslemma2dlem0b  15527  gausslemma2dlem0c  15528  lgsquadlem2  15555  lgsquad2lem2  15559  2lgsoddprmlem2  15583  2sqlem8  15600  gropd  15644  grstructd2dom  15645  bj-nnan  15672  bj-charfun  15743  bdop  15811  bdunexb  15856  bj-om  15873  findset  15881  bj-peano4  15891  bj-inf2vn  15910  bj-inf2vn2  15911  pwle2  15935  pwf1oexmid  15936  nnnninfex  15959  sbthom  15965  qdencn  15966  trilpolemlt1  15980