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  759  ordi  823  stdcndc  852  stdcndcOLD  853  dfandc  891  mpbi2and  951  mpbir2and  952  pm4.82  958  pm4.83dc  959  rnlem  984  ifp2  988  syl22anc  1274  syl112anc  1277  syl121anc  1278  syl211anc  1279  syl23anc  1280  syl32anc  1281  syl122anc  1282  syl212anc  1283  syl221anc  1284  syl222anc  1289  syl123anc  1290  syl132anc  1291  syl213anc  1292  syl231anc  1293  syl312anc  1294  syl321anc  1295  syl223anc  1299  syl232anc  1300  syl322anc  1301  syl233anc  1302  syl323anc  1303  syl332anc  1304  ecased  1385  19.26  1529  nfand  1616  19.40  1679  equsexd  1777  sbcof2  1858  sbequ8  1895  eu2  2124  eu3h  2125  eu5  2127  mooran2  2153  datisi  2190  felapton  2194  darapti  2195  dimatis  2197  fresison  2198  fesapo  2200  reximssdv  2636  r19.26  2659  r19.29af2  2673  r19.40  2687  eqvinc  2929  eqvincg  2930  elrabd  2964  reu6  2995  reu3  2996  indifdir  3463  undif3ss  3468  un00  3541  eqifdc  3642  disjpr2  3733  prel12  3854  prneimg  3857  preqsn  3858  disjiun  4083  opth  4329  0nelop  4340  euotd  4347  opelopabsb  4354  ispod  4401  elon2  4473  unexb  4539  opeluu  4547  eusvnfb  4551  suc11g  4655  nlimsucg  4664  tfi  4680  vtoclr  4774  opthprc  4777  ideqg  4881  resiexg  5058  dminss  5151  imainss  5152  ssxpbm  5172  relrelss  5263  funopg  5360  fununfun  5373  fntpg  5386  fun11uni  5400  imain  5412  funimaexglem  5413  funssxp  5504  ffdm  5505  f00  5528  dffo2  5563  fodmrnu  5567  foco  5570  fun11iun  5604  f1o00  5620  fsnd  5628  fv3  5662  dff2  5791  dff3im  5792  dffo4  5795  ffnfv  5805  ffvresb  5810  fsn2  5821  fconstfvm  5871  fnfvima  5888  resfvresima  5890  fcof1o  5929  isocnv  5951  isotr  5956  riotaprop  5996  acexmidlemcase  6012  caovlem2d  6214  f1ocnvd  6224  caofcom  6265  resfunexgALT  6269  elxp7  6332  2ndrn  6345  1stconst  6385  2ndconst  6386  cnvf1olem  6388  poxp  6396  dftpos4  6428  dfsmo2  6452  tfrlem5  6479  tfrlemiex  6496  tfr1onlemsucaccv  6506  tfr1onlembfn  6509  tfr1onlemex  6512  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembfn  6522  tfrcllemex  6525  tfrcllemres  6527  tfrcl  6529  frecabex  6563  frecabcl  6564  frecfcllem  6569  frecrdg  6573  oawordi  6636  nntri3  6664  nntr2  6670  nnmordi  6683  iserd  6727  relelec  6743  erth  6747  qliftfun  6785  mapsncnv  6863  mptelixpg  6902  bren  6916  pw2f1odclem  7019  findcard2d  7079  findcard2sd  7080  isinfinf  7085  tridc  7088  nnwetri  7107  undifdcss  7114  fiintim  7122  fisseneq  7126  fidcenumlemim  7150  sbthlemi9  7163  supisolem  7206  ordiso2  7233  updjud  7280  difinfsn  7298  ctssdccl  7309  nnnninfeq  7326  omniwomnimkv  7365  pr2cv  7401  acfun  7421  exmidontriimlem2  7436  onntri45  7458  dftap2  7469  netap  7472  2omotaplemap  7475  ccfunen  7482  cc4f  7487  cc4n  7489  elni2  7533  dfplpq2  7573  dfmpq2  7574  enqbreq2  7576  enqdc1  7581  addcmpblnq  7586  addclnq  7594  nqpi  7597  addassnqg  7601  mulassnqg  7603  mulcanenq  7604  distrnqg  7606  1qec  7607  recexnq  7609  subhalfnqq  7633  enq0tr  7653  nqnq0pi  7657  nq0nn  7661  mulcanenq0ec  7664  nnnq0lem1  7665  addclnq0  7670  distrnq0  7678  addassnq0lemcl  7680  elnp1st2nd  7695  prarloc  7722  addlocprlemlt  7750  addlocprlemeq  7752  addlocprlemgt  7753  addclpr  7756  nqprm  7761  mullocprlem  7789  mullocpr  7790  mulclpr  7791  ltpopr  7814  ltaddpr  7816  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemrnd  7824  ltexprlemdisj  7825  addcanprleml  7833  addcanprlemu  7834  addcanprg  7835  recexprlemm  7843  recexprlemopl  7844  recexprlemopu  7846  recexprlemrnd  7848  recexprlemdisj  7849  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemrnd  7869  cauappcvgprlemdisj  7870  cauappcvgprlemlim  7880  caucvgprlemnkj  7885  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemrnd  7892  caucvgprlemlim  7900  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  caucvgprprlemm  7915  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemrnd  7920  caucvgprprlemexbt  7925  caucvgprprlemlim  7930  suplocexprlemrl  7936  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  prsrlem1  7961  mulclsr  7973  mulasssrg  7977  distrsrg  7978  suplocsrlemb  8025  elreal2  8049  axmulass  8092  axdistr  8093  axcaucvglemcau  8117  add20  8653  mullt0  8659  rereim  8765  ltmul1  8771  cru  8781  mulap0r  8794  aprcl  8825  aptap  8829  divmuldivap  8891  divmuleqap  8896  divadddivap  8906  divmuldivapd  9011  divmuleqapd  9012  div2subap  9016  ltmul12a  9039  lemul12a  9041  lemulge11  9045  lediv12a  9073  lediv2a  9074  recgt1i  9077  recreclt  9079  ledivp1  9082  lemul1ad  9118  lemul2ad  9119  ltmul12ad  9120  lemul12ad  9121  lemul12bd  9122  nndivre  9178  nndivtr  9184  halfaddsubcl  9376  halfaddsub  9377  lt2halves  9379  nnrecl  9399  elnn0nn  9443  elnnnn0b  9445  elnnnn0c  9446  nn0addge1  9447  nn0addge2  9448  xnn0xrnemnf  9476  elnn0z  9491  elnnz1  9501  nzadd  9531  elz2  9550  zdivadd  9568  zdivmul  9569  zextle  9570  peano2uz2  9586  uzind  9590  btwnz  9598  uzss  9776  eluzp1m1  9779  infregelbex  9831  eluz2b2  9836  qre  9858  qaddcl  9868  qmulcl  9870  qreccl  9875  irradd  9879  irrmul  9880  elpqb  9883  cnref1o  9884  rprege0  9902  rprene0  9905  rpreap0  9906  rpcnne0  9907  rpcnap0  9908  rpregt0d  9937  rprege0d  9938  rprene0d  9939  rpcnne0d  9940  lediv2ad  9953  ledivge1le  9960  lediv12ad  9990  nnledivrp  10000  nn0ledivnn  10001  xrlttri3  10031  xrrebnd  10053  xrrege0  10059  xnn0xadd0  10101  xlesubadd  10117  elioo4g  10168  ioomax  10182  iccmax  10183  divelunit  10236  elfz5  10251  uzsubsubfz  10281  fzopth  10295  fzass4  10296  fzrev2  10319  uzsplit  10326  elfz2nn0  10346  difelfzle  10368  1fv  10373  4fvwrd4  10374  fzo1fzo0n0  10421  elfzom1elp1fzo  10446  subfzo0  10487  infssuzex  10492  qtri3or  10499  adddivflid  10551  flltdivnn0lt  10563  intfracq  10581  modqid2  10612  modfzo0difsn  10656  seq3val  10721  seqvalcd  10722  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemmo  10766  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seqf1oglem1  10780  seqf1oglem2  10781  expclzaplem  10824  leexp1a  10855  expubnd  10857  le2sq2  10876  sumsqeq0  10879  bernneq  10921  expnlbnd  10925  nn0opthd  10983  faclbnd6  11005  facavg  11007  seq3coll  11105  hash2en  11106  wrdnval  11143  ccat0  11172  ccatsymb  11178  ccatalpha  11189  swrdspsleq  11247  pfxtrcfv  11273  pfxsuffeqwrdeq  11278  wrd2ind  11303  pfxccatin12lem2a  11307  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  pfxccatpfx1  11316  pfxccatpfx2  11317  swrdccatin1d  11323  swrdccatin2d  11324  shftlem  11376  shftfvalg  11378  shftfval  11381  cvg1nlemcau  11544  cvg1nlemres  11545  rexuz3  11550  resqrexlemcvg  11579  resqrexlemglsq  11582  resqrexlemga  11583  sqrtle  11596  sqrtlt  11597  sqrt11  11599  sqrtsq2  11603  absmul  11629  sqabs  11642  abslt  11648  absle  11649  lenegsq  11655  maxleastb  11774  maxltsup  11778  rexanre  11780  negfi  11788  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxltsup  11818  xrmaxadd  11821  climcn2  11869  mulcn2  11872  summodclem2a  11941  summodc  11943  fsum3  11947  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  fsump1i  11993  fsum0diaglem  12000  mptfzshft  12002  fsumrev  12003  fsummulc2  12008  fsum00  12022  expcnvap0  12062  mertenslemi1  12095  ntrivcvgap0  12109  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodrev  12179  fprodconst  12180  eftlub  12250  efieq  12295  sincos1sgn  12325  demoivreALT  12334  dvdsval3  12351  dvdscmul  12378  dvdsmulc  12379  dvdscmulr  12380  dvdsmulcr  12381  modmulconst  12383  dvds2ln  12384  ltoddhalfle  12453  nn0o  12467  divalg2  12486  ndvdssub  12490  ndvdsadd  12491  divgcdz  12541  gcd0id  12549  gcdaddm  12554  bezoutlemstep  12567  bezoutlemmain  12568  dfgcd3  12580  dfgcd2  12584  lcmcllem  12638  dvdslcm  12640  lcmgcdlem  12648  lcmgcdnn  12653  qredeq  12667  qredeu  12668  rpdvds  12670  divgcdcoprm0  12672  cncongr1  12674  cncongr2  12675  cncongrcoprm  12677  prmind2  12691  isprm5  12713  isprm6  12718  prmexpb  12722  cncongrprm  12728  sqrt2irrlem  12732  pw2dvdslemn  12736  oddpwdclemxy  12740  oddpwdclemdc  12744  oddpwdc  12745  hashdvds  12792  prmdiv  12806  hashgcdlem  12809  nnoddn2prmb  12834  pythagtriplem6  12842  pythagtriplem7  12843  pcpre1  12864  pccl  12871  pcmul  12873  pcdiv  12874  pcqmul  12875  pcqcl  12878  pcdvds  12887  pcndvds  12889  pcndvds2  12891  pc2dvds  12902  dvdsprmpweqle  12909  difsqpwdvds  12910  pcaddlem  12911  pcadd  12912  pcmptcl  12914  pcmpt  12915  fldivp1  12920  pcfac  12922  oddprmdvds  12926  infpnlem2  12932  4sqlem5  12954  4sqlem6  12955  4sqlem4a  12963  4sqexercise1  12970  4sqexercise2  12971  4sqlem13m  12975  4sqlem15  12977  4sqlem16  12978  ennnfonelemfun  13037  ennnfonelemim  13044  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  ctiunctlemfo  13059  omctfn  13063  fnpr2ob  13422  ismgmid2  13462  fngsum  13470  igsumvalx  13471  gsumfzval  13473  gsum0g  13478  gsumval2  13479  issgrpd  13494  ismndd  13519  prdsidlem  13529  imasmnd2  13534  mhmf1o  13552  subsubm  13565  dfgrp2  13609  isgrpid2  13622  isgrpinv  13636  grplrinv  13639  dfgrp3mlem  13680  dfgrp3m  13681  dfgrp3me  13682  prdsinvlem  13690  imasgrp2  13696  mhmmnd  13702  issubg2m  13775  issubgrpd2  13776  grpissubg  13780  subsubg  13783  subgintm  13784  isnsg3  13793  nmzsubg  13796  eqgval  13809  eqgen  13813  isghmd  13838  ghmrn  13843  ghmpreima  13852  ghmf1o  13861  conjghm  13862  conjnmzb  13866  ghmpropd  13869  rinvmod  13895  imasabl  13922  rnglz  13957  isrngd  13965  srgdilem  13981  srglmhm  14005  srgrmhm  14006  ringdilem  14024  isringd  14053  ringsrg  14059  ringinvnzdiv  14062  imasring  14076  dvdsrd  14107  unitgrp  14129  isrim0  14174  isrhm2d  14178  rhmf1o  14181  rhmco  14187  rhmopp  14189  issubrng2  14223  subsubrng  14227  subrgugrp  14253  issubrg2  14254  subsubrg  14258  resrhm  14261  aprap  14299  lmodfopnelem2  14338  lsssubg  14390  islss3  14392  islss4  14395  lspsnel6  14421  lidlacl  14497  lidlsubg  14499  lidlrsppropdg  14508  2idlelbas  14529  cnfld1  14585  cnsubglem  14592  mulgghm2  14621  zndvds  14662  mplsubgfi  14714  topgele  14752  tgcl  14787  epttop  14813  opnssneib  14879  iscnp4  14941  cnco  14944  cncnp  14953  cnrest2  14959  lmss  14969  txcnp  14994  txcn  14998  cnmpt12  15010  cnmpt22  15017  hmeof1o  15032  psmetres2  15056  distspace  15058  ismeti  15069  isxmetd  15070  xmetpsmet  15092  xblss2ps  15127  xblss2  15128  blcntrps  15138  blcntr  15139  blin2  15155  mopni3  15207  metequiv2  15219  bdmet  15225  xmettx  15233  cnbl0  15257  cnblcld  15258  tgioo  15277  elcncf1di  15302  dedekindeulemlu  15344  suplociccex  15348  dedekindicclemlu  15353  dedekindicc  15356  ivthinclemlopn  15359  ivthdec  15367  ivthreinc  15368  ivthdichlem  15374  cnplimcim  15390  limccnp2lem  15399  dvfvalap  15404  plymullem  15473  reeff1olem  15494  sin0pilem1  15504  pilem3  15506  ptolemy  15547  sincosq1sgn  15549  sinq12gt0  15553  ioocosf1o  15577  rprelogbmulexp  15679  perfectlem2  15723  lgslem3  15730  lgsne0  15766  gausslemma2dlem0b  15778  gausslemma2dlem0c  15779  lgsquadlem2  15806  lgsquad2lem2  15810  2lgsoddprmlem2  15834  2sqlem8  15851  gropd  15897  grstructd2dom  15898  incistruhgr  15940  umgrislfupgrenlem  15980  umgrislfupgrdom  15981  uspgrupgrushgr  16032  usgrumgruspgr  16035  usgruspgrben  16036  usgrislfuspgrdom  16040  umgrvad2edg  16061  umgr2edgneu  16062  ushgredgedg  16076  ushgredgedgloop  16078  subgrprop3  16112  iswlkg  16179  wlk2f  16201  upgriswlkdc  16210  wlkv0  16219  wlklenvclwlk  16223  wlkepvtx  16225  upgr2wlkdc  16227  wlkres  16229  clwwlkccatlem  16250  clwwlkccat  16251  clwwlknbp  16265  clwwlknp  16267  clwwlkext2edg  16272  clwwlknon  16279  clwwlknonccat  16283  clwwlknonex2  16289  clwwlknonex2e  16290  trlsegvdeglem1  16310  bj-nnan  16332  bj-charfun  16402  bdop  16470  bdunexb  16515  bj-om  16532  findset  16540  bj-peano4  16550  bj-inf2vn  16569  bj-inf2vn2  16570  pwle2  16599  pwf1oexmid  16600  nnnninfex  16624  sbthom  16630  qdencn  16631  trilpolemlt1  16645  gfsumval  16680