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  5430  ffdm  5431  f00  5452  dffo2  5487  fodmrnu  5491  foco  5494  fun11iun  5528  f1o00  5542  fsnd  5550  fv3  5584  dff2  5709  dff3im  5710  dffo4  5713  ffnfv  5723  ffvresb  5728  fsn2  5739  fconstfvm  5783  fnfvima  5800  fcof1o  5839  isocnv  5861  isotr  5866  riotaprop  5904  acexmidlemcase  5920  caovlem2d  6120  f1ocnvd  6129  caofcom  6170  resfunexgALT  6174  elxp7  6237  2ndrn  6250  1stconst  6288  2ndconst  6289  cnvf1olem  6291  poxp  6299  dftpos4  6330  dfsmo2  6354  tfrlem5  6381  tfrlemiex  6398  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfr1onlemex  6414  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcllemex  6427  tfrcllemres  6429  tfrcl  6431  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecrdg  6475  oawordi  6536  nntri3  6564  nntr2  6570  nnmordi  6583  iserd  6627  relelec  6643  erth  6647  qliftfun  6685  mapsncnv  6763  mptelixpg  6802  bren  6815  pw2f1odclem  6904  findcard2d  6961  findcard2sd  6962  isinfinf  6967  tridc  6969  nnwetri  6986  undifdcss  6993  fiintim  7001  fisseneq  7004  fidcenumlemim  7027  sbthlemi9  7040  supisolem  7083  ordiso2  7110  updjud  7157  difinfsn  7175  ctssdccl  7186  nnnninfeq  7203  omniwomnimkv  7242  acfun  7292  exmidontriimlem2  7307  onntri45  7326  dftap2  7336  netap  7339  2omotaplemap  7342  ccfunen  7349  cc4f  7354  cc4n  7356  elni2  7400  dfplpq2  7440  dfmpq2  7441  enqbreq2  7443  enqdc1  7448  addcmpblnq  7453  addclnq  7461  nqpi  7464  addassnqg  7468  mulassnqg  7470  mulcanenq  7471  distrnqg  7473  1qec  7474  recexnq  7476  subhalfnqq  7500  enq0tr  7520  nqnq0pi  7524  nq0nn  7528  mulcanenq0ec  7531  nnnq0lem1  7532  addclnq0  7537  distrnq0  7545  addassnq0lemcl  7547  elnp1st2nd  7562  prarloc  7589  addlocprlemlt  7617  addlocprlemeq  7619  addlocprlemgt  7620  addclpr  7623  nqprm  7628  mullocprlem  7656  mullocpr  7657  mulclpr  7658  ltpopr  7681  ltaddpr  7683  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemrnd  7691  ltexprlemdisj  7692  addcanprleml  7700  addcanprlemu  7701  addcanprg  7702  recexprlemm  7710  recexprlemopl  7711  recexprlemopu  7713  recexprlemrnd  7715  recexprlemdisj  7716  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemrnd  7736  cauappcvgprlemdisj  7737  cauappcvgprlemlim  7747  caucvgprlemnkj  7752  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemrnd  7759  caucvgprlemlim  7767  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  caucvgprprlemm  7782  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemrnd  7787  caucvgprprlemexbt  7792  caucvgprprlemlim  7797  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  prsrlem1  7828  mulclsr  7840  mulasssrg  7844  distrsrg  7845  suplocsrlemb  7892  elreal2  7916  axmulass  7959  axdistr  7960  axcaucvglemcau  7984  add20  8520  mullt0  8526  rereim  8632  ltmul1  8638  cru  8648  mulap0r  8661  aprcl  8692  aptap  8696  divmuldivap  8758  divmuleqap  8763  divadddivap  8773  divmuldivapd  8878  divmuleqapd  8879  div2subap  8883  ltmul12a  8906  lemul12a  8908  lemulge11  8912  lediv12a  8940  lediv2a  8941  recgt1i  8944  recreclt  8946  ledivp1  8949  lemul1ad  8985  lemul2ad  8986  ltmul12ad  8987  lemul12ad  8988  lemul12bd  8989  nndivre  9045  nndivtr  9051  halfaddsubcl  9243  halfaddsub  9244  lt2halves  9246  nnrecl  9266  elnn0nn  9310  elnnnn0b  9312  elnnnn0c  9313  nn0addge1  9314  nn0addge2  9315  xnn0xrnemnf  9343  elnn0z  9358  elnnz1  9368  nzadd  9397  elz2  9416  zdivadd  9434  zdivmul  9435  zextle  9436  peano2uz2  9452  uzind  9456  btwnz  9464  uzss  9641  eluzp1m1  9644  infregelbex  9691  eluz2b2  9696  qre  9718  qaddcl  9728  qmulcl  9730  qreccl  9735  irradd  9739  irrmul  9740  elpqb  9743  cnref1o  9744  rprege0  9762  rprene0  9765  rpreap0  9766  rpcnne0  9767  rpcnap0  9768  rpregt0d  9797  rprege0d  9798  rprene0d  9799  rpcnne0d  9800  lediv2ad  9813  ledivge1le  9820  lediv12ad  9850  nnledivrp  9860  nn0ledivnn  9861  xrlttri3  9891  xrrebnd  9913  xrrege0  9919  xnn0xadd0  9961  xlesubadd  9977  elioo4g  10028  ioomax  10042  iccmax  10043  divelunit  10096  elfz5  10111  uzsubsubfz  10141  fzopth  10155  fzass4  10156  fzrev2  10179  uzsplit  10186  elfz2nn0  10206  difelfzle  10228  1fv  10233  4fvwrd4  10234  fzo1fzo0n0  10278  elfzom1elp1fzo  10297  subfzo0  10337  infssuzex  10342  qtri3or  10349  adddivflid  10401  flltdivnn0lt  10413  intfracq  10431  modqid2  10462  modfzo0difsn  10506  seq3val  10571  seqvalcd  10572  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemmo  10616  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seqf1oglem1  10630  seqf1oglem2  10631  expclzaplem  10674  leexp1a  10705  expubnd  10707  le2sq2  10726  sumsqeq0  10729  bernneq  10771  expnlbnd  10775  nn0opthd  10833  faclbnd6  10855  facavg  10857  seq3coll  10953  wrdnval  10984  shftlem  11000  shftfvalg  11002  shftfval  11005  cvg1nlemcau  11168  cvg1nlemres  11169  rexuz3  11174  resqrexlemcvg  11203  resqrexlemglsq  11206  resqrexlemga  11207  sqrtle  11220  sqrtlt  11221  sqrt11  11223  sqrtsq2  11227  absmul  11253  sqabs  11266  abslt  11272  absle  11273  lenegsq  11279  maxleastb  11398  maxltsup  11402  rexanre  11404  negfi  11412  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxltsup  11442  xrmaxadd  11445  climcn2  11493  mulcn2  11496  summodclem2a  11565  summodc  11567  fsum3  11571  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fsump1i  11617  fsum0diaglem  11624  mptfzshft  11626  fsumrev  11627  fsummulc2  11632  fsum00  11646  expcnvap0  11686  mertenslemi1  11719  ntrivcvgap0  11733  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodrev  11803  fprodconst  11804  eftlub  11874  efieq  11919  sincos1sgn  11949  demoivreALT  11958  dvdsval3  11975  dvdscmul  12002  dvdsmulc  12003  dvdscmulr  12004  dvdsmulcr  12005  modmulconst  12007  dvds2ln  12008  ltoddhalfle  12077  nn0o  12091  divalg2  12110  ndvdssub  12114  ndvdsadd  12115  divgcdz  12165  gcd0id  12173  gcdaddm  12178  bezoutlemstep  12191  bezoutlemmain  12192  dfgcd3  12204  dfgcd2  12208  lcmcllem  12262  dvdslcm  12264  lcmgcdlem  12272  lcmgcdnn  12277  qredeq  12291  qredeu  12292  rpdvds  12294  divgcdcoprm0  12296  cncongr1  12298  cncongr2  12299  cncongrcoprm  12301  prmind2  12315  isprm5  12337  isprm6  12342  prmexpb  12346  cncongrprm  12352  sqrt2irrlem  12356  pw2dvdslemn  12360  oddpwdclemxy  12364  oddpwdclemdc  12368  oddpwdc  12369  hashdvds  12416  prmdiv  12430  hashgcdlem  12433  nnoddn2prmb  12458  pythagtriplem6  12466  pythagtriplem7  12467  pcpre1  12488  pccl  12495  pcmul  12497  pcdiv  12498  pcqmul  12499  pcqcl  12502  pcdvds  12511  pcndvds  12513  pcndvds2  12515  pc2dvds  12526  dvdsprmpweqle  12533  difsqpwdvds  12534  pcaddlem  12535  pcadd  12536  pcmptcl  12538  pcmpt  12539  fldivp1  12544  pcfac  12546  oddprmdvds  12550  infpnlem2  12556  4sqlem5  12578  4sqlem6  12579  4sqlem4a  12587  4sqexercise1  12594  4sqexercise2  12595  4sqlem13m  12599  4sqlem15  12601  4sqlem16  12602  ennnfonelemfun  12661  ennnfonelemim  12668  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  ctiunctlemfo  12683  omctfn  12687  fnpr2ob  13044  ismgmid2  13084  fngsum  13092  igsumvalx  13093  gsumfzval  13095  gsum0g  13100  gsumval2  13101  issgrpd  13116  ismndd  13141  prdsidlem  13151  imasmnd2  13156  mhmf1o  13174  subsubm  13187  dfgrp2  13231  isgrpid2  13244  isgrpinv  13258  grplrinv  13261  dfgrp3mlem  13302  dfgrp3m  13303  dfgrp3me  13304  prdsinvlem  13312  imasgrp2  13318  mhmmnd  13324  issubg2m  13397  issubgrpd2  13398  grpissubg  13402  subsubg  13405  subgintm  13406  isnsg3  13415  nmzsubg  13418  eqgval  13431  eqgen  13435  isghmd  13460  ghmrn  13465  ghmpreima  13474  ghmf1o  13483  conjghm  13484  conjnmzb  13488  ghmpropd  13491  rinvmod  13517  imasabl  13544  rnglz  13579  isrngd  13587  srgdilem  13603  srglmhm  13627  srgrmhm  13628  ringdilem  13646  isringd  13675  ringsrg  13681  ringinvnzdiv  13684  imasring  13698  dvdsrd  13728  unitgrp  13750  isrim0  13795  isrhm2d  13799  rhmf1o  13802  rhmco  13808  rhmopp  13810  issubrng2  13844  subsubrng  13848  subrgugrp  13874  issubrg2  13875  subsubrg  13879  resrhm  13882  aprap  13920  lmodfopnelem2  13959  lsssubg  14011  islss3  14013  islss4  14016  lspsnel6  14042  lidlacl  14118  lidlsubg  14120  lidlrsppropdg  14129  2idlelbas  14150  cnfld1  14206  cnsubglem  14213  mulgghm2  14242  zndvds  14283  mplsubgfi  14335  topgele  14373  tgcl  14408  epttop  14434  opnssneib  14500  iscnp4  14562  cnco  14565  cncnp  14574  cnrest2  14580  lmss  14590  txcnp  14615  txcn  14619  cnmpt12  14631  cnmpt22  14638  hmeof1o  14653  psmetres2  14677  distspace  14679  ismeti  14690  isxmetd  14691  xmetpsmet  14713  xblss2ps  14748  xblss2  14749  blcntrps  14759  blcntr  14760  blin2  14776  mopni3  14828  metequiv2  14840  bdmet  14846  xmettx  14854  cnbl0  14878  cnblcld  14879  tgioo  14898  elcncf1di  14923  dedekindeulemlu  14965  suplociccex  14969  dedekindicclemlu  14974  dedekindicc  14977  ivthinclemlopn  14980  ivthdec  14988  ivthreinc  14989  ivthdichlem  14995  cnplimcim  15011  limccnp2lem  15020  dvfvalap  15025  plymullem  15094  reeff1olem  15115  sin0pilem1  15125  pilem3  15127  ptolemy  15168  sincosq1sgn  15170  sinq12gt0  15174  ioocosf1o  15198  rprelogbmulexp  15300  perfectlem2  15344  lgslem3  15351  lgsne0  15387  gausslemma2dlem0b  15399  gausslemma2dlem0c  15400  lgsquadlem2  15427  lgsquad2lem2  15431  2lgsoddprmlem2  15455  2sqlem8  15472  bj-nnan  15490  bj-charfun  15561  bdop  15629  bdunexb  15674  bj-om  15691  findset  15699  bj-peano4  15709  bj-inf2vn  15728  bj-inf2vn2  15729  pwle2  15753  pwf1oexmid  15754  nnnninfex  15777  sbthom  15783  qdencn  15784  trilpolemlt1  15798