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  ioran  752  ordi  816  stdcndc  845  stdcndcOLD  846  dfandc  884  pm4.55dc  938  mpbi2and  943  mpbir2and  944  pm4.82  950  pm4.83dc  951  rnlem  976  syl22anc  1239  syl112anc  1242  syl121anc  1243  syl211anc  1244  syl23anc  1245  syl32anc  1246  syl122anc  1247  syl212anc  1248  syl221anc  1249  syl222anc  1254  syl123anc  1255  syl132anc  1256  syl213anc  1257  syl231anc  1258  syl312anc  1259  syl321anc  1260  syl223anc  1264  syl232anc  1265  syl322anc  1266  syl233anc  1267  syl323anc  1268  syl332anc  1269  ecased  1349  19.26  1479  nfand  1566  19.40  1629  equsexd  1727  sbcof2  1808  sbequ8  1845  eu2  2068  eu3h  2069  eu5  2071  mooran2  2097  datisi  2134  felapton  2138  darapti  2139  dimatis  2141  fresison  2142  fesapo  2144  reximssdv  2579  r19.26  2601  r19.29af2  2615  r19.40  2629  eqvinc  2858  eqvincg  2859  elrabd  2893  reu6  2924  reu3  2925  indifdir  3389  undif3ss  3394  un00  3467  eqifdc  3566  disjpr2  3653  prel12  3767  prneimg  3770  preqsn  3771  disjiun  3993  opth  4231  0nelop  4242  euotd  4248  opelopabsb  4254  ispod  4298  elon2  4370  unexb  4436  opeluu  4444  eusvnfb  4448  suc11g  4550  nlimsucg  4559  tfi  4575  vtoclr  4668  opthprc  4671  ideqg  4771  resiexg  4945  dminss  5035  imainss  5036  ssxpbm  5056  relrelss  5147  funopg  5242  fntpg  5264  fun11uni  5278  imain  5290  funimaexglem  5291  funssxp  5377  ffdm  5378  f00  5399  dffo2  5434  fodmrnu  5438  foco  5440  fun11iun  5474  f1o00  5488  fsnd  5496  fv3  5530  dff2  5652  dff3im  5653  dffo4  5656  ffnfv  5666  ffvresb  5671  fsn2  5682  fconstfvm  5726  fnfvima  5742  fcof1o  5780  isocnv  5802  isotr  5807  riotaprop  5844  acexmidlemcase  5860  caovlem2d  6057  f1ocnvd  6063  caofcom  6096  resfunexgALT  6099  elxp7  6161  2ndrn  6174  1stconst  6212  2ndconst  6213  cnvf1olem  6215  poxp  6223  dftpos4  6254  dfsmo2  6278  tfrlem5  6305  tfrlemiex  6322  tfr1onlemsucaccv  6332  tfr1onlembfn  6335  tfr1onlemex  6338  tfr1onlemres  6340  tfrcllemsucaccv  6345  tfrcllembfn  6348  tfrcllemex  6351  tfrcllemres  6353  tfrcl  6355  frecabex  6389  frecabcl  6390  frecfcllem  6395  frecrdg  6399  oawordi  6460  nntri3  6488  nntr2  6494  nnmordi  6507  iserd  6551  relelec  6565  erth  6569  qliftfun  6607  mapsncnv  6685  mptelixpg  6724  bren  6737  findcard2d  6881  findcard2sd  6882  isinfinf  6887  tridc  6889  nnwetri  6905  undifdcss  6912  fiintim  6918  fisseneq  6921  fidcenumlemim  6941  sbthlemi9  6954  supisolem  6997  ordiso2  7024  updjud  7071  difinfsn  7089  ctssdccl  7100  nnnninfeq  7116  omniwomnimkv  7155  acfun  7196  exmidontriimlem2  7211  onntri45  7230  ccfunen  7238  cc4f  7243  cc4n  7245  elni2  7288  dfplpq2  7328  dfmpq2  7329  enqbreq2  7331  enqdc1  7336  addcmpblnq  7341  addclnq  7349  nqpi  7352  addassnqg  7356  mulassnqg  7358  mulcanenq  7359  distrnqg  7361  1qec  7362  recexnq  7364  subhalfnqq  7388  enq0tr  7408  nqnq0pi  7412  nq0nn  7416  mulcanenq0ec  7419  nnnq0lem1  7420  addclnq0  7425  distrnq0  7433  addassnq0lemcl  7435  elnp1st2nd  7450  prarloc  7477  addlocprlemlt  7505  addlocprlemeq  7507  addlocprlemgt  7508  addclpr  7511  nqprm  7516  mullocprlem  7544  mullocpr  7545  mulclpr  7546  ltpopr  7569  ltaddpr  7571  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemrnd  7579  ltexprlemdisj  7580  addcanprleml  7588  addcanprlemu  7589  addcanprg  7590  recexprlemm  7598  recexprlemopl  7599  recexprlemopu  7601  recexprlemrnd  7603  recexprlemdisj  7604  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemrnd  7624  cauappcvgprlemdisj  7625  cauappcvgprlemlim  7635  caucvgprlemnkj  7640  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemrnd  7647  caucvgprlemlim  7655  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnjltk  7665  caucvgprprlemm  7670  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemrnd  7675  caucvgprprlemexbt  7680  caucvgprprlemlim  7685  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  prsrlem1  7716  mulclsr  7728  mulasssrg  7732  distrsrg  7733  suplocsrlemb  7780  elreal2  7804  axmulass  7847  axdistr  7848  axcaucvglemcau  7872  add20  8405  mullt0  8411  rereim  8517  ltmul1  8523  cru  8533  mulap0r  8546  aprcl  8577  divmuldivap  8641  divmuleqap  8646  divadddivap  8656  divmuldivapd  8761  divmuleqapd  8762  div2subap  8766  ltmul12a  8788  lemul12a  8790  lemulge11  8794  lediv12a  8822  lediv2a  8823  recgt1i  8826  recreclt  8828  ledivp1  8831  lemul1ad  8867  lemul2ad  8868  ltmul12ad  8869  lemul12ad  8870  lemul12bd  8871  nndivre  8926  nndivtr  8932  halfaddsubcl  9123  halfaddsub  9124  lt2halves  9125  nnrecl  9145  elnn0nn  9189  elnnnn0b  9191  elnnnn0c  9192  nn0addge1  9193  nn0addge2  9194  xnn0xrnemnf  9222  elnn0z  9237  elnnz1  9247  nzadd  9276  elz2  9295  zdivadd  9313  zdivmul  9314  zextle  9315  peano2uz2  9331  uzind  9335  btwnz  9343  uzss  9519  eluzp1m1  9522  infregelbex  9569  eluz2b2  9574  qre  9596  qaddcl  9606  qmulcl  9608  qreccl  9613  irradd  9617  irrmul  9618  elpqb  9620  cnref1o  9621  rprege0  9637  rprene0  9640  rpreap0  9641  rpcnne0  9642  rpcnap0  9643  rpregt0d  9672  rprege0d  9673  rprene0d  9674  rpcnne0d  9675  lediv2ad  9688  ledivge1le  9695  lediv12ad  9725  nnledivrp  9735  nn0ledivnn  9736  xrlttri3  9766  xrrebnd  9788  xrrege0  9794  xnn0xadd0  9836  xlesubadd  9852  elioo4g  9903  ioomax  9917  iccmax  9918  divelunit  9971  elfz5  9985  uzsubsubfz  10015  fzopth  10029  fzass4  10030  fzrev2  10053  uzsplit  10060  elfz2nn0  10080  difelfzle  10102  1fv  10107  4fvwrd4  10108  fzo1fzo0n0  10151  elfzom1elp1fzo  10170  subfzo0  10210  qtri3or  10211  adddivflid  10260  flltdivnn0lt  10272  intfracq  10288  modqid2  10319  modfzo0difsn  10363  seq3val  10426  seqvalcd  10427  iseqf1olemqcl  10454  iseqf1olemnab  10456  iseqf1olemab  10457  iseqf1olemmo  10460  seq3f1olemqsumkj  10466  seq3f1olemqsumk  10467  expclzaplem  10512  leexp1a  10543  expubnd  10545  le2sq2  10563  sumsqeq0  10566  bernneq  10608  expnlbnd  10612  nn0opthd  10668  faclbnd6  10690  facavg  10692  seq3coll  10788  shftlem  10791  shftfvalg  10793  shftfval  10796  cvg1nlemcau  10959  cvg1nlemres  10960  rexuz3  10965  resqrexlemcvg  10994  resqrexlemglsq  10997  resqrexlemga  10998  sqrtle  11011  sqrtlt  11012  sqrt11  11014  sqrtsq2  11018  absmul  11044  sqabs  11057  abslt  11063  absle  11064  lenegsq  11070  maxleastb  11189  maxltsup  11193  rexanre  11195  negfi  11202  xrmaxiflemab  11221  xrmaxiflemlub  11222  xrmaxltsup  11232  xrmaxadd  11235  climcn2  11283  mulcn2  11286  summodclem2a  11355  summodc  11357  fsum3  11361  fsum3cvg3  11370  fsumcl2lem  11372  fsumadd  11380  fsump1i  11407  fsum0diaglem  11414  mptfzshft  11416  fsumrev  11417  fsummulc2  11422  fsum00  11436  expcnvap0  11476  mertenslemi1  11509  ntrivcvgap0  11523  prodmodclem3  11549  prodmodclem2a  11550  zproddc  11553  fprodseq  11557  fprodrev  11593  fprodconst  11594  eftlub  11664  efieq  11709  sincos1sgn  11738  demoivreALT  11747  dvdsval3  11764  dvdscmul  11791  dvdsmulc  11792  dvdscmulr  11793  dvdsmulcr  11794  modmulconst  11796  dvds2ln  11797  ltoddhalfle  11863  nn0o  11877  divalg2  11896  ndvdssub  11900  ndvdsadd  11901  infssuzex  11915  divgcdz  11937  gcd0id  11945  gcdaddm  11950  bezoutlemstep  11963  bezoutlemmain  11964  dfgcd3  11976  dfgcd2  11980  lcmcllem  12032  dvdslcm  12034  lcmgcdlem  12042  lcmgcdnn  12047  qredeq  12061  qredeu  12062  rpdvds  12064  divgcdcoprm0  12066  cncongr1  12068  cncongr2  12069  cncongrcoprm  12071  prmind2  12085  isprm5  12107  isprm6  12112  prmexpb  12116  cncongrprm  12122  sqrt2irrlem  12126  pw2dvdslemn  12130  oddpwdclemxy  12134  oddpwdclemdc  12138  oddpwdc  12139  hashdvds  12186  prmdiv  12200  hashgcdlem  12203  nnoddn2prmb  12227  pythagtriplem6  12235  pythagtriplem7  12236  pcpre1  12257  pccl  12264  pcmul  12266  pcdiv  12267  pcqmul  12268  pcqcl  12271  pcdvds  12279  pcndvds  12281  pcndvds2  12283  pc2dvds  12294  dvdsprmpweqle  12301  difsqpwdvds  12302  pcaddlem  12303  pcadd  12304  pcmptcl  12305  pcmpt  12306  fldivp1  12311  pcfac  12313  oddprmdvds  12317  infpnlem2  12323  4sqlem5  12345  4sqlem6  12346  4sqlem4a  12354  ennnfonelemfun  12383  ennnfonelemim  12390  ctinfomlemom  12393  ctinfom  12394  ctinf  12396  ctiunctlemfo  12405  omctfn  12409  ismgmid2  12663  ismndd  12702  mhmf1o  12722  dfgrp2  12762  isgrpid2  12773  isgrpinv  12786  grplrinv  12787  dfgrp3mlem  12827  dfgrp3m  12828  dfgrp3me  12829  mhmmnd  12839  rinvmod  12909  srgdilem  12947  srglmhm  12971  srgrmhm  12972  ringdilem  12990  isringd  13014  ringsrg  13018  ringinvnzdiv  13021  topgele  13096  tgcl  13133  epttop  13159  opnssneib  13225  iscnp4  13287  cnco  13290  cncnp  13299  cnrest2  13305  lmss  13315  txcnp  13340  txcn  13344  cnmpt12  13356  cnmpt22  13363  hmeof1o  13378  psmetres2  13402  distspace  13404  ismeti  13415  isxmetd  13416  xmetpsmet  13438  xblss2ps  13473  xblss2  13474  blcntrps  13484  blcntr  13485  blin2  13501  mopni3  13553  metequiv2  13565  bdmet  13571  xmettx  13579  cnbl0  13603  cnblcld  13604  tgioo  13615  elcncf1di  13635  dedekindeulemlu  13668  suplociccex  13672  dedekindicclemlu  13677  dedekindicc  13680  ivthinclemlopn  13683  ivthdec  13691  cnplimcim  13705  limccnp2lem  13714  dvfvalap  13719  reeff1olem  13761  sin0pilem1  13771  pilem3  13773  ptolemy  13814  sincosq1sgn  13816  sinq12gt0  13820  ioocosf1o  13844  rprelogbmulexp  13943  lgslem3  13972  lgsne0  14008  2sqlem8  14028  bj-nnan  14046  bj-charfun  14117  bdop  14185  bdunexb  14230  bj-om  14247  findset  14255  bj-peano4  14265  bj-inf2vn  14284  bj-inf2vn2  14285  pwle2  14306  pwf1oexmid  14307  sbthom  14333  qdencn  14334  trilpolemlt1  14348