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  1492  nfand  1579  19.40  1642  equsexd  1740  sbcof2  1821  sbequ8  1858  eu2  2086  eu3h  2087  eu5  2089  mooran2  2115  datisi  2152  felapton  2156  darapti  2157  dimatis  2159  fresison  2160  fesapo  2162  reximssdv  2598  r19.26  2620  r19.29af2  2634  r19.40  2648  eqvinc  2883  eqvincg  2884  elrabd  2918  reu6  2949  reu3  2950  indifdir  3415  undif3ss  3420  un00  3493  eqifdc  3592  disjpr2  3682  prel12  3797  prneimg  3800  preqsn  3801  disjiun  4024  opth  4266  0nelop  4277  euotd  4283  opelopabsb  4290  ispod  4335  elon2  4407  unexb  4473  opeluu  4481  eusvnfb  4485  suc11g  4589  nlimsucg  4598  tfi  4614  vtoclr  4707  opthprc  4710  ideqg  4813  resiexg  4987  dminss  5080  imainss  5081  ssxpbm  5101  relrelss  5192  funopg  5288  fntpg  5310  fun11uni  5324  imain  5336  funimaexglem  5337  funssxp  5423  ffdm  5424  f00  5445  dffo2  5480  fodmrnu  5484  foco  5487  fun11iun  5521  f1o00  5535  fsnd  5543  fv3  5577  dff2  5702  dff3im  5703  dffo4  5706  ffnfv  5716  ffvresb  5721  fsn2  5732  fconstfvm  5776  fnfvima  5793  fcof1o  5832  isocnv  5854  isotr  5859  riotaprop  5897  acexmidlemcase  5913  caovlem2d  6111  f1ocnvd  6120  caofcom  6156  resfunexgALT  6160  elxp7  6223  2ndrn  6236  1stconst  6274  2ndconst  6275  cnvf1olem  6277  poxp  6285  dftpos4  6316  dfsmo2  6340  tfrlem5  6367  tfrlemiex  6384  tfr1onlemsucaccv  6394  tfr1onlembfn  6397  tfr1onlemex  6400  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllembfn  6410  tfrcllemex  6413  tfrcllemres  6415  tfrcl  6417  frecabex  6451  frecabcl  6452  frecfcllem  6457  frecrdg  6461  oawordi  6522  nntri3  6550  nntr2  6556  nnmordi  6569  iserd  6613  relelec  6629  erth  6633  qliftfun  6671  mapsncnv  6749  mptelixpg  6788  bren  6801  pw2f1odclem  6890  findcard2d  6947  findcard2sd  6948  isinfinf  6953  tridc  6955  nnwetri  6972  undifdcss  6979  fiintim  6985  fisseneq  6988  fidcenumlemim  7011  sbthlemi9  7024  supisolem  7067  ordiso2  7094  updjud  7141  difinfsn  7159  ctssdccl  7170  nnnninfeq  7187  omniwomnimkv  7226  acfun  7267  exmidontriimlem2  7282  onntri45  7301  dftap2  7311  netap  7314  2omotaplemap  7317  ccfunen  7324  cc4f  7329  cc4n  7331  elni2  7374  dfplpq2  7414  dfmpq2  7415  enqbreq2  7417  enqdc1  7422  addcmpblnq  7427  addclnq  7435  nqpi  7438  addassnqg  7442  mulassnqg  7444  mulcanenq  7445  distrnqg  7447  1qec  7448  recexnq  7450  subhalfnqq  7474  enq0tr  7494  nqnq0pi  7498  nq0nn  7502  mulcanenq0ec  7505  nnnq0lem1  7506  addclnq0  7511  distrnq0  7519  addassnq0lemcl  7521  elnp1st2nd  7536  prarloc  7563  addlocprlemlt  7591  addlocprlemeq  7593  addlocprlemgt  7594  addclpr  7597  nqprm  7602  mullocprlem  7630  mullocpr  7631  mulclpr  7632  ltpopr  7655  ltaddpr  7657  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemrnd  7665  ltexprlemdisj  7666  addcanprleml  7674  addcanprlemu  7675  addcanprg  7676  recexprlemm  7684  recexprlemopl  7685  recexprlemopu  7687  recexprlemrnd  7689  recexprlemdisj  7690  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemrnd  7710  cauappcvgprlemdisj  7711  cauappcvgprlemlim  7721  caucvgprlemnkj  7726  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemrnd  7733  caucvgprlemlim  7741  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnjltk  7751  caucvgprprlemm  7756  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemrnd  7761  caucvgprprlemexbt  7766  caucvgprprlemlim  7771  suplocexprlemrl  7777  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  prsrlem1  7802  mulclsr  7814  mulasssrg  7818  distrsrg  7819  suplocsrlemb  7866  elreal2  7890  axmulass  7933  axdistr  7934  axcaucvglemcau  7958  add20  8493  mullt0  8499  rereim  8605  ltmul1  8611  cru  8621  mulap0r  8634  aprcl  8665  aptap  8669  divmuldivap  8731  divmuleqap  8736  divadddivap  8746  divmuldivapd  8851  divmuleqapd  8852  div2subap  8856  ltmul12a  8879  lemul12a  8881  lemulge11  8885  lediv12a  8913  lediv2a  8914  recgt1i  8917  recreclt  8919  ledivp1  8922  lemul1ad  8958  lemul2ad  8959  ltmul12ad  8960  lemul12ad  8961  lemul12bd  8962  nndivre  9018  nndivtr  9024  halfaddsubcl  9215  halfaddsub  9216  lt2halves  9218  nnrecl  9238  elnn0nn  9282  elnnnn0b  9284  elnnnn0c  9285  nn0addge1  9286  nn0addge2  9287  xnn0xrnemnf  9315  elnn0z  9330  elnnz1  9340  nzadd  9369  elz2  9388  zdivadd  9406  zdivmul  9407  zextle  9408  peano2uz2  9424  uzind  9428  btwnz  9436  uzss  9613  eluzp1m1  9616  infregelbex  9663  eluz2b2  9668  qre  9690  qaddcl  9700  qmulcl  9702  qreccl  9707  irradd  9711  irrmul  9712  elpqb  9715  cnref1o  9716  rprege0  9734  rprene0  9737  rpreap0  9738  rpcnne0  9739  rpcnap0  9740  rpregt0d  9769  rprege0d  9770  rprene0d  9771  rpcnne0d  9772  lediv2ad  9785  ledivge1le  9792  lediv12ad  9822  nnledivrp  9832  nn0ledivnn  9833  xrlttri3  9863  xrrebnd  9885  xrrege0  9891  xnn0xadd0  9933  xlesubadd  9949  elioo4g  10000  ioomax  10014  iccmax  10015  divelunit  10068  elfz5  10083  uzsubsubfz  10113  fzopth  10127  fzass4  10128  fzrev2  10151  uzsplit  10158  elfz2nn0  10178  difelfzle  10200  1fv  10205  4fvwrd4  10206  fzo1fzo0n0  10250  elfzom1elp1fzo  10269  subfzo0  10309  qtri3or  10310  adddivflid  10361  flltdivnn0lt  10373  intfracq  10391  modqid2  10422  modfzo0difsn  10466  seq3val  10531  seqvalcd  10532  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemmo  10576  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seqf1oglem1  10590  seqf1oglem2  10591  expclzaplem  10634  leexp1a  10665  expubnd  10667  le2sq2  10686  sumsqeq0  10689  bernneq  10731  expnlbnd  10735  nn0opthd  10793  faclbnd6  10815  facavg  10817  seq3coll  10913  wrdnval  10944  shftlem  10960  shftfvalg  10962  shftfval  10965  cvg1nlemcau  11128  cvg1nlemres  11129  rexuz3  11134  resqrexlemcvg  11163  resqrexlemglsq  11166  resqrexlemga  11167  sqrtle  11180  sqrtlt  11181  sqrt11  11183  sqrtsq2  11187  absmul  11213  sqabs  11226  abslt  11232  absle  11233  lenegsq  11239  maxleastb  11358  maxltsup  11362  rexanre  11364  negfi  11371  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxltsup  11401  xrmaxadd  11404  climcn2  11452  mulcn2  11455  summodclem2a  11524  summodc  11526  fsum3  11530  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  fsump1i  11576  fsum0diaglem  11583  mptfzshft  11585  fsumrev  11586  fsummulc2  11591  fsum00  11605  expcnvap0  11645  mertenslemi1  11678  ntrivcvgap0  11692  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodrev  11762  fprodconst  11763  eftlub  11833  efieq  11878  sincos1sgn  11908  demoivreALT  11917  dvdsval3  11934  dvdscmul  11961  dvdsmulc  11962  dvdscmulr  11963  dvdsmulcr  11964  modmulconst  11966  dvds2ln  11967  ltoddhalfle  12034  nn0o  12048  divalg2  12067  ndvdssub  12071  ndvdsadd  12072  infssuzex  12086  divgcdz  12108  gcd0id  12116  gcdaddm  12121  bezoutlemstep  12134  bezoutlemmain  12135  dfgcd3  12147  dfgcd2  12151  lcmcllem  12205  dvdslcm  12207  lcmgcdlem  12215  lcmgcdnn  12220  qredeq  12234  qredeu  12235  rpdvds  12237  divgcdcoprm0  12239  cncongr1  12241  cncongr2  12242  cncongrcoprm  12244  prmind2  12258  isprm5  12280  isprm6  12285  prmexpb  12289  cncongrprm  12295  sqrt2irrlem  12299  pw2dvdslemn  12303  oddpwdclemxy  12307  oddpwdclemdc  12311  oddpwdc  12312  hashdvds  12359  prmdiv  12373  hashgcdlem  12376  nnoddn2prmb  12400  pythagtriplem6  12408  pythagtriplem7  12409  pcpre1  12430  pccl  12437  pcmul  12439  pcdiv  12440  pcqmul  12441  pcqcl  12444  pcdvds  12453  pcndvds  12455  pcndvds2  12457  pc2dvds  12468  dvdsprmpweqle  12475  difsqpwdvds  12476  pcaddlem  12477  pcadd  12478  pcmptcl  12480  pcmpt  12481  fldivp1  12486  pcfac  12488  oddprmdvds  12492  infpnlem2  12498  4sqlem5  12520  4sqlem6  12521  4sqlem4a  12529  4sqexercise1  12536  4sqexercise2  12537  4sqlem13m  12541  4sqlem15  12543  4sqlem16  12544  ennnfonelemfun  12574  ennnfonelemim  12581  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  ctiunctlemfo  12596  omctfn  12600  fnpr2ob  12923  ismgmid2  12963  fngsum  12971  igsumvalx  12972  gsumfzval  12974  gsum0g  12979  gsumval2  12980  issgrpd  12995  ismndd  13018  mhmf1o  13042  subsubm  13055  dfgrp2  13099  isgrpid2  13112  isgrpinv  13126  grplrinv  13129  dfgrp3mlem  13170  dfgrp3m  13171  dfgrp3me  13172  imasgrp2  13180  mhmmnd  13186  issubg2m  13259  issubgrpd2  13260  grpissubg  13264  subsubg  13267  subgintm  13268  isnsg3  13277  nmzsubg  13280  eqgval  13293  eqgen  13297  isghmd  13322  ghmrn  13327  ghmpreima  13336  ghmf1o  13345  conjghm  13346  conjnmzb  13350  ghmpropd  13353  rinvmod  13379  imasabl  13406  rnglz  13441  isrngd  13449  srgdilem  13465  srglmhm  13489  srgrmhm  13490  ringdilem  13508  isringd  13537  ringsrg  13543  ringinvnzdiv  13546  imasring  13560  dvdsrd  13590  unitgrp  13612  isrim0  13657  isrhm2d  13661  rhmf1o  13664  rhmco  13670  rhmopp  13672  issubrng2  13706  subsubrng  13710  subrgugrp  13736  issubrg2  13737  subsubrg  13741  resrhm  13744  aprap  13782  lmodfopnelem2  13821  lsssubg  13873  islss3  13875  islss4  13878  lspsnel6  13904  lidlacl  13980  lidlsubg  13982  lidlrsppropdg  13991  2idlelbas  14012  cnfld1  14060  cnsubglem  14067  mulgghm2  14096  zndvds  14137  topgele  14197  tgcl  14232  epttop  14258  opnssneib  14324  iscnp4  14386  cnco  14389  cncnp  14398  cnrest2  14404  lmss  14414  txcnp  14439  txcn  14443  cnmpt12  14455  cnmpt22  14462  hmeof1o  14477  psmetres2  14501  distspace  14503  ismeti  14514  isxmetd  14515  xmetpsmet  14537  xblss2ps  14572  xblss2  14573  blcntrps  14583  blcntr  14584  blin2  14600  mopni3  14652  metequiv2  14664  bdmet  14670  xmettx  14678  cnbl0  14702  cnblcld  14703  tgioo  14714  elcncf1di  14734  dedekindeulemlu  14775  suplociccex  14779  dedekindicclemlu  14784  dedekindicc  14787  ivthinclemlopn  14790  ivthdec  14798  ivthreinc  14799  ivthdichlem  14805  cnplimcim  14821  limccnp2lem  14830  dvfvalap  14835  plymullem  14896  reeff1olem  14906  sin0pilem1  14916  pilem3  14918  ptolemy  14959  sincosq1sgn  14961  sinq12gt0  14965  ioocosf1o  14989  rprelogbmulexp  15088  lgslem3  15118  lgsne0  15154  gausslemma2dlem0b  15166  gausslemma2dlem0c  15167  2lgsoddprmlem2  15194  2sqlem8  15210  bj-nnan  15228  bj-charfun  15299  bdop  15367  bdunexb  15412  bj-om  15429  findset  15437  bj-peano4  15447  bj-inf2vn  15466  bj-inf2vn2  15467  pwle2  15489  pwf1oexmid  15490  sbthom  15516  qdencn  15517  trilpolemlt1  15531