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  607  biadanid  618  ioran  760  ordi  824  stdcndc  853  stdcndcOLD  854  dfandc  892  mpbi2and  952  mpbir2and  953  pm4.82  959  pm4.83dc  960  rnlem  985  ifp2  989  syl22anc  1275  syl112anc  1278  syl121anc  1279  syl211anc  1280  syl23anc  1281  syl32anc  1282  syl122anc  1283  syl212anc  1284  syl221anc  1285  syl222anc  1290  syl123anc  1291  syl132anc  1292  syl213anc  1293  syl231anc  1294  syl312anc  1295  syl321anc  1296  syl223anc  1300  syl232anc  1301  syl322anc  1302  syl233anc  1303  syl323anc  1304  syl332anc  1305  ecased  1386  19.26  1530  nfand  1617  19.40  1680  equsexd  1778  sbcof2  1859  sbequ8  1896  eu2  2125  eu3h  2126  eu5  2128  mooran2  2154  datisi  2191  felapton  2195  darapti  2196  dimatis  2198  fresison  2199  fesapo  2201  reximssdv  2646  r19.26  2669  r19.29af2  2683  r19.40  2697  eqvinc  2940  eqvincg  2941  elrabd  2975  reu6  3006  reu3  3007  indifdir  3477  undif3ss  3482  un00  3555  eqifdc  3659  disjpr2  3753  prel12  3875  prneimg  3878  preqsn  3879  disjiun  4104  opth  4353  0nelop  4364  euotd  4371  opelopabsb  4378  ispod  4425  elon2  4497  unexb  4563  opeluu  4571  eusvnfb  4575  suc11g  4679  nlimsucg  4688  tfi  4704  vtoclr  4798  opthprc  4801  ideqg  4906  resiexg  5083  dminss  5177  imainss  5178  ssxpbm  5198  relrelss  5289  funopg  5386  fununfun  5399  fntpg  5412  fun11uni  5426  imain  5438  funimaexglem  5439  funssxp  5532  ffdm  5533  f00  5559  dffo2  5594  fodmrnu  5598  foco  5601  fun11iun  5635  f1o00  5651  fsnd  5659  fv3  5693  dff2  5821  dff3im  5822  dffo4  5825  ffnfv  5835  ffvresb  5840  fsn2  5851  fconstfvm  5902  fnfvima  5921  resfvresima  5923  fcof1o  5962  isocnv  5984  isotr  5989  riotaprop  6029  acexmidlemcase  6045  caovlem2d  6247  f1ocnvd  6257  caofcom  6297  resfunexgALT  6301  elxp7  6364  2ndrn  6377  1stconst  6417  2ndconst  6418  cnvf1olem  6420  poxp  6428  ressuppss  6454  funsssuppss  6458  dftpos4  6494  dfsmo2  6518  tfrlem5  6545  tfrlemiex  6562  tfr1onlemsucaccv  6572  tfr1onlembfn  6575  tfr1onlemex  6578  tfr1onlemres  6580  tfrcllemsucaccv  6585  tfrcllembfn  6588  tfrcllemex  6591  tfrcllemres  6593  tfrcl  6595  frecabex  6629  frecabcl  6630  frecfcllem  6635  frecrdg  6639  oawordi  6702  nntri3  6730  nntr2  6736  nnmordi  6749  iserd  6793  relelec  6809  erth  6813  qliftfun  6851  mapsnd  6923  mapsncnv  6930  mptelixpg  6969  bren  6983  pw2f1odclem  7087  mapunen  7104  findcard2d  7148  findcard2sd  7149  isinfinf  7154  tridc  7157  nnwetri  7176  undifdcss  7183  fiintim  7191  fisseneq  7195  fidcenumlemim  7222  sbthlemi9  7235  supisolem  7299  ordiso2  7326  updjud  7373  difinfsn  7391  ctssdccl  7402  nnnninfeq  7419  omniwomnimkv  7458  pr2cv  7494  acfun  7514  exmidontriimlem2  7529  onntri45  7551  dftap2  7565  netap  7568  2omotaplemap  7571  ccfunen  7578  cc4f  7583  cc4n  7585  elni2  7629  dfplpq2  7669  dfmpq2  7670  enqbreq2  7672  enqdc1  7677  addcmpblnq  7682  addclnq  7690  nqpi  7693  addassnqg  7697  mulassnqg  7699  mulcanenq  7700  distrnqg  7702  1qec  7703  recexnq  7705  subhalfnqq  7729  enq0tr  7749  nqnq0pi  7753  nq0nn  7757  mulcanenq0ec  7760  nnnq0lem1  7761  addclnq0  7766  distrnq0  7774  addassnq0lemcl  7776  elnp1st2nd  7791  prarloc  7818  addlocprlemlt  7846  addlocprlemeq  7848  addlocprlemgt  7849  addclpr  7852  nqprm  7857  mullocprlem  7885  mullocpr  7886  mulclpr  7887  ltpopr  7910  ltaddpr  7912  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemrnd  7920  ltexprlemdisj  7921  addcanprleml  7929  addcanprlemu  7930  addcanprg  7931  recexprlemm  7939  recexprlemopl  7940  recexprlemopu  7942  recexprlemrnd  7944  recexprlemdisj  7945  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemrnd  7965  cauappcvgprlemdisj  7966  cauappcvgprlemlim  7976  caucvgprlemnkj  7981  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemrnd  7988  caucvgprlemlim  7996  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnjltk  8006  caucvgprprlemm  8011  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemrnd  8016  caucvgprprlemexbt  8021  caucvgprprlemlim  8026  suplocexprlemrl  8032  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  prsrlem1  8057  mulclsr  8069  mulasssrg  8073  distrsrg  8074  suplocsrlemb  8121  elreal2  8145  axmulass  8188  axdistr  8189  axcaucvglemcau  8213  add20  8748  mullt0  8754  rereim  8860  ltmul1  8866  cru  8876  mulap0r  8889  aprcl  8920  aptap  8924  divmuldivap  8986  divmuleqap  8991  divadddivap  9001  divmuldivapd  9106  divmuleqapd  9107  div2subap  9111  ltmul12a  9134  lemul12a  9136  lemulge11  9140  lediv12a  9168  lediv2a  9169  recgt1i  9172  recreclt  9174  ledivp1  9177  lemul1ad  9213  lemul2ad  9214  ltmul12ad  9215  lemul12ad  9216  lemul12bd  9217  nndivre  9273  nndivtr  9279  halfaddsubcl  9471  halfaddsub  9472  lt2halves  9474  nnrecl  9494  elnn0nn  9538  elnnnn0b  9540  elnnnn0c  9541  nn0addge1  9542  nn0addge2  9543  xnn0xrnemnf  9575  elnn0z  9590  elnnz1  9600  nzadd  9630  elz2  9649  zdivadd  9667  zdivmul  9668  zextle  9669  peano2uz2  9685  uzind  9689  btwnz  9697  uzss  9875  eluzp1m1  9878  infregelbex  9930  eluz2b2  9935  qre  9957  qaddcl  9967  qmulcl  9969  qreccl  9974  irradd  9978  irrmul  9979  elpqb  9982  cnref1o  9983  rprege0  10001  rprene0  10004  rpreap0  10005  rpcnne0  10006  rpcnap0  10007  rpregt0d  10036  rprege0d  10037  rprene0d  10038  rpcnne0d  10039  lediv2ad  10052  ledivge1le  10059  lediv12ad  10089  nnledivrp  10099  nn0ledivnn  10100  xrlttri3  10130  xrrebnd  10152  xrrege0  10158  xnn0xadd0  10200  xlesubadd  10216  elioo4g  10267  ioomax  10281  iccmax  10282  divelunit  10335  elfz5  10351  uzsubsubfz  10381  fzopth  10395  fzass4  10396  fzrev2  10419  uzsplit  10426  elfz2nn0  10446  difelfzle  10468  1fv  10473  4fvwrd4  10474  fzo1fzo0n0  10522  elfzom1elp1fzo  10547  subfzo0  10588  infssuzex  10593  qtri3or  10600  adddivflid  10652  flltdivnn0lt  10664  intfracq  10682  modqid2  10713  modfzo0difsn  10757  seq3val  10822  seqvalcd  10823  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemmo  10867  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seqf1oglem1  10881  seqf1oglem2  10882  expclzaplem  10925  leexp1a  10956  expubnd  10958  le2sq2  10977  sumsqeq0  10980  bernneq  11022  expnlbnd  11026  nn0opthd  11084  faclbnd6  11106  facavg  11108  sseqn  11203  hashfibclem  11206  seq3coll  11214  hash2en  11215  wrdnval  11255  ccat0  11284  ccatsymb  11290  ccatalpha  11301  swrdspsleq  11359  pfxtrcfv  11385  pfxsuffeqwrdeq  11390  wrd2ind  11415  pfxccatin12lem2a  11419  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  pfxccatpfx1  11428  pfxccatpfx2  11429  swrdccatin1d  11435  swrdccatin2d  11436  shftlem  11501  shftfvalg  11503  shftfval  11506  cvg1nlemcau  11669  cvg1nlemres  11670  rexuz3  11675  resqrexlemcvg  11704  resqrexlemglsq  11707  resqrexlemga  11708  sqrtle  11721  sqrtlt  11722  sqrt11  11724  sqrtsq2  11728  absmul  11754  sqabs  11767  abslt  11773  absle  11774  lenegsq  11780  maxleastb  11899  maxltsup  11903  rexanre  11905  negfi  11913  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxltsup  11943  xrmaxadd  11946  climcn2  11994  mulcn2  11997  summodclem2a  12067  summodc  12069  fsum3  12073  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  fsump1i  12119  fsum0diaglem  12126  mptfzshft  12128  fsumrev  12129  fsummulc2  12134  fsum00  12148  expcnvap0  12188  mertenslemi1  12221  ntrivcvgap0  12235  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodrev  12305  fprodconst  12306  eftlub  12376  efieq  12421  sincos1sgn  12451  demoivreALT  12460  dvdsval3  12477  dvdscmul  12504  dvdsmulc  12505  dvdscmulr  12506  dvdsmulcr  12507  modmulconst  12509  dvds2ln  12510  ltoddhalfle  12579  nn0o  12593  divalg2  12612  ndvdssub  12616  ndvdsadd  12617  divgcdz  12667  gcd0id  12675  gcdaddm  12680  bezoutlemstep  12693  bezoutlemmain  12694  dfgcd3  12706  dfgcd2  12710  lcmcllem  12764  dvdslcm  12766  lcmgcdlem  12774  lcmgcdnn  12779  qredeq  12793  qredeu  12794  rpdvds  12796  divgcdcoprm0  12798  cncongr1  12800  cncongr2  12801  cncongrcoprm  12803  prmind2  12817  isprm5  12839  isprm6  12844  prmexpb  12848  cncongrprm  12854  sqrt2irrlem  12858  pw2dvdslemn  12862  oddpwdclemxy  12866  oddpwdclemdc  12870  oddpwdc  12871  hashdvds  12918  prmdiv  12932  hashgcdlem  12935  nnoddn2prmb  12960  pythagtriplem6  12968  pythagtriplem7  12969  pcpre1  12990  pccl  12997  pcmul  12999  pcdiv  13000  pcqmul  13001  pcqcl  13004  pcdvds  13013  pcndvds  13015  pcndvds2  13017  pc2dvds  13028  dvdsprmpweqle  13035  difsqpwdvds  13036  pcaddlem  13037  pcadd  13038  pcmptcl  13040  pcmpt  13041  fldivp1  13046  pcfac  13048  oddprmdvds  13052  infpnlem2  13058  4sqlem5  13080  4sqlem6  13081  4sqlem4a  13089  4sqexercise1  13096  4sqexercise2  13097  4sqlem13m  13101  4sqlem15  13103  4sqlem16  13104  ballotfilem2  13142  ennnfonelemfun  13168  ennnfonelemim  13175  ctinfomlemom  13178  ctinfom  13179  ctinf  13181  ctiunctlemfo  13190  omctfn  13194  fnpr2ob  13553  ismgmid2  13593  fngsum  13601  igsumvalx  13602  gsumfzval  13604  gsum0g  13609  gsumval2  13610  issgrpd  13625  ismndd  13650  prdsidlem  13660  imasmnd2  13665  mhmf1o  13683  subsubm  13696  dfgrp2  13740  isgrpid2  13753  isgrpinv  13767  grplrinv  13770  dfgrp3mlem  13811  dfgrp3m  13812  dfgrp3me  13813  prdsinvlem  13821  imasgrp2  13827  mhmmnd  13833  issubg2m  13906  issubgrpd2  13907  grpissubg  13911  subsubg  13914  subgintm  13915  isnsg3  13924  nmzsubg  13927  eqgval  13940  eqgen  13944  isghmd  13969  ghmrn  13974  ghmpreima  13983  ghmf1o  13992  conjghm  13993  conjnmzb  13997  ghmpropd  14000  rinvmod  14026  imasabl  14053  rnglz  14089  isrngd  14097  srgdilem  14113  srglmhm  14137  srgrmhm  14138  ringdilem  14156  isringd  14185  ringsrg  14191  ringinvnzdiv  14194  imasring  14208  dvdsrd  14239  unitgrp  14261  isrim0  14306  isrhm2d  14310  rhmf1o  14313  rhmco  14319  rhmopp  14321  issubrng2  14355  subsubrng  14359  subrgugrp  14385  issubrg2  14386  subsubrg  14390  resrhm  14393  aprap  14432  lmodfopnelem2  14473  lsssubg  14525  islss3  14527  islss4  14530  lspsnel6  14556  lidlacl  14632  lidlsubg  14634  lidlrsppropdg  14643  2idlelbas  14664  cnfld1  14720  cnsubglem  14727  mulgghm2  14756  zndvds  14797  psrbagcon  14826  mplsubgfi  14856  topgele  14894  tgcl  14929  epttop  14955  opnssneib  15021  iscnp4  15083  cnco  15086  cncnp  15095  cnrest2  15101  lmss  15111  txcnp  15136  txcn  15140  cnmpt12  15152  cnmpt22  15159  hmeof1o  15174  psmetres2  15198  distspace  15200  ismeti  15211  isxmetd  15212  xmetpsmet  15234  xblss2ps  15269  xblss2  15270  blcntrps  15280  blcntr  15281  blin2  15297  mopni3  15349  metequiv2  15361  bdmet  15367  xmettx  15375  cnbl0  15399  cnblcld  15400  tgioo  15419  elcncf1di  15444  dedekindeulemlu  15486  suplociccex  15490  dedekindicclemlu  15495  dedekindicc  15498  ivthinclemlopn  15501  ivthdec  15509  ivthreinc  15510  ivthdichlem  15516  cnplimcim  15532  limccnp2lem  15541  dvfvalap  15546  plymullem  15615  reeff1olem  15636  sin0pilem1  15646  pilem3  15648  ptolemy  15689  sincosq1sgn  15691  sinq12gt0  15695  ioocosf1o  15719  rprelogbmulexp  15821  pellexlem3  15847  perfectlem2  15868  lgslem3  15875  lgsne0  15911  gausslemma2dlem0b  15923  gausslemma2dlem0c  15924  lgsquadlem2  15951  lgsquad2lem2  15955  2lgsoddprmlem2  15979  2sqlem8  15996  gropd  16042  grstructd2dom  16043  incistruhgr  16085  umgrislfupgrenlem  16125  umgrislfupgrdom  16126  uspgrupgrushgr  16177  usgrumgruspgr  16180  usgruspgrben  16181  usgrislfuspgrdom  16185  umgrvad2edg  16206  umgr2edgneu  16207  ushgredgedg  16221  ushgredgedgloop  16223  subgrprop3  16257  iswlkg  16324  wlk2f  16346  upgriswlkdc  16355  wlkv0  16364  wlklenvclwlk  16368  wlkepvtx  16370  upgr2wlkdc  16372  wlkres  16374  clwwlkccatlem  16395  clwwlkccat  16396  clwwlknbp  16410  clwwlknp  16412  clwwlkext2edg  16417  clwwlknon  16424  clwwlknonccat  16428  clwwlknonex2  16434  clwwlknonex2e  16435  trlsegvdeglem1  16455  bj-nnan  16508  bj-charfun  16577  bdop  16645  bdunexb  16690  bj-om  16707  findset  16715  bj-peano4  16725  bj-inf2vn  16744  bj-inf2vn2  16745  pwle2  16772  pwf1oexmid  16773  nnnninfex  16800  sbthom  16806  qdencn  16807  trilpolemlt1  16825  gfsumval  16862  gfsump1  16868