Theorem jca 304

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 138	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒)))
4	1, 2, 3	sylc 62	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jca31  307  jca32  308  jcai  309  jctil  310  jctir  311  ancli  321  ancri  322  sylanbrc  414  jcab  593  ioran  742  ordi  806  stdcndc  835  stdcndcOLD  836  dfandc  874  pm4.55dc  927  mpbi2and  932  mpbir2and  933  pm4.82  939  pm4.83dc  940  rnlem  965  syl22anc  1228  syl112anc  1231  syl121anc  1232  syl211anc  1233  syl23anc  1234  syl32anc  1235  syl122anc  1236  syl212anc  1237  syl221anc  1238  syl222anc  1243  syl123anc  1244  syl132anc  1245  syl213anc  1246  syl231anc  1247  syl312anc  1248  syl321anc  1249  syl223anc  1253  syl232anc  1254  syl322anc  1255  syl233anc  1256  syl323anc  1257  syl332anc  1258  ecased  1338  19.26  1468  nfand  1555  19.40  1618  equsexd  1716  sbcof2  1797  sbequ8  1834  eu2  2057  eu3h  2058  eu5  2060  mooran2  2086  datisi  2123  felapton  2127  darapti  2128  dimatis  2130  fresison  2131  fesapo  2133  reximssdv  2568  r19.26  2590  r19.29af2  2604  r19.40  2618  eqvinc  2844  eqvincg  2845  elrabd  2879  reu6  2910  reu3  2911  indifdir  3373  undif3ss  3378  un00  3450  eqifdc  3549  disjpr2  3634  prel12  3745  prneimg  3748  preqsn  3749  disjiun  3971  opth  4209  0nelop  4220  euotd  4226  opelopabsb  4232  ispod  4276  elon2  4348  unexb  4414  opeluu  4422  eusvnfb  4426  suc11g  4528  nlimsucg  4537  tfi  4553  vtoclr  4646  opthprc  4649  ideqg  4749  resiexg  4923  dminss  5012  imainss  5013  ssxpbm  5033  relrelss  5124  funopg  5216  fntpg  5238  fun11uni  5252  imain  5264  funimaexglem  5265  funssxp  5351  ffdm  5352  f00  5373  dffo2  5408  fodmrnu  5412  foco  5414  fun11iun  5447  f1o00  5461  fsnd  5469  fv3  5503  dff2  5623  dff3im  5624  dffo4  5627  ffnfv  5637  ffvresb  5642  fsn2  5653  fconstfvm  5697  fnfvima  5713  fcof1o  5751  isocnv  5773  isotr  5778  riotaprop  5815  acexmidlemcase  5831  caovlem2d  6025  f1ocnvd  6034  caofcom  6067  resfunexgALT  6070  elxp7  6130  2ndrn  6143  1stconst  6180  2ndconst  6181  cnvf1olem  6183  poxp  6191  dftpos4  6222  dfsmo2  6246  tfrlem5  6273  tfrlemiex  6290  tfr1onlemsucaccv  6300  tfr1onlembfn  6303  tfr1onlemex  6306  tfr1onlemres  6308  tfrcllemsucaccv  6313  tfrcllembfn  6316  tfrcllemex  6319  tfrcllemres  6321  tfrcl  6323  frecabex  6357  frecabcl  6358  frecfcllem  6363  frecrdg  6367  oawordi  6428  nntri3  6456  nntr2  6462  nnmordi  6475  iserd  6518  relelec  6532  erth  6536  qliftfun  6574  mapsncnv  6652  mptelixpg  6691  bren  6704  findcard2d  6848  findcard2sd  6849  isinfinf  6854  tridc  6856  nnwetri  6872  undifdcss  6879  fiintim  6885  fisseneq  6888  fidcenumlemim  6908  sbthlemi9  6921  supisolem  6964  ordiso2  6991  updjud  7038  difinfsn  7056  ctssdccl  7067  nnnninfeq  7083  omniwomnimkv  7122  acfun  7154  exmidontriimlem2  7169  onntri45  7188  ccfunen  7196  cc4f  7201  cc4n  7203  elni2  7246  dfplpq2  7286  dfmpq2  7287  enqbreq2  7289  enqdc1  7294  addcmpblnq  7299  addclnq  7307  nqpi  7310  addassnqg  7314  mulassnqg  7316  mulcanenq  7317  distrnqg  7319  1qec  7320  recexnq  7322  subhalfnqq  7346  enq0tr  7366  nqnq0pi  7370  nq0nn  7374  mulcanenq0ec  7377  nnnq0lem1  7378  addclnq0  7383  distrnq0  7391  addassnq0lemcl  7393  elnp1st2nd  7408  prarloc  7435  addlocprlemlt  7463  addlocprlemeq  7465  addlocprlemgt  7466  addclpr  7469  nqprm  7474  mullocprlem  7502  mullocpr  7503  mulclpr  7504  ltpopr  7527  ltaddpr  7529  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemrnd  7537  ltexprlemdisj  7538  addcanprleml  7546  addcanprlemu  7547  addcanprg  7548  recexprlemm  7556  recexprlemopl  7557  recexprlemopu  7559  recexprlemrnd  7561  recexprlemdisj  7562  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemopu  7580  cauappcvgprlemrnd  7582  cauappcvgprlemdisj  7583  cauappcvgprlemlim  7593  caucvgprlemnkj  7598  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemopu  7603  caucvgprlemrnd  7605  caucvgprlemlim  7613  caucvgprprlemnkltj  7621  caucvgprprlemnkeqj  7622  caucvgprprlemnjltk  7623  caucvgprprlemm  7628  caucvgprprlemopl  7629  caucvgprprlemopu  7631  caucvgprprlemrnd  7633  caucvgprprlemexbt  7638  caucvgprprlemlim  7643  suplocexprlemrl  7649  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemex  7654  suplocexprlemub  7655  prsrlem1  7674  mulclsr  7686  mulasssrg  7690  distrsrg  7691  suplocsrlemb  7738  elreal2  7762  axmulass  7805  axdistr  7806  axcaucvglemcau  7830  add20  8363  mullt0  8369  rereim  8475  ltmul1  8481  cru  8491  mulap0r  8504  aprcl  8535  divmuldivap  8599  divmuleqap  8604  divadddivap  8614  divmuldivapd  8719  divmuleqapd  8720  div2subap  8724  ltmul12a  8746  lemul12a  8748  lemulge11  8752  lediv12a  8780  lediv2a  8781  recgt1i  8784  recreclt  8786  ledivp1  8789  lemul1ad  8825  lemul2ad  8826  ltmul12ad  8827  lemul12ad  8828  lemul12bd  8829  nndivre  8884  nndivtr  8890  halfaddsubcl  9081  halfaddsub  9082  lt2halves  9083  nnrecl  9103  elnn0nn  9147  elnnnn0b  9149  elnnnn0c  9150  nn0addge1  9151  nn0addge2  9152  xnn0xrnemnf  9180  elnn0z  9195  elnnz1  9205  nzadd  9234  elz2  9253  zdivadd  9271  zdivmul  9272  zextle  9273  peano2uz2  9289  uzind  9293  btwnz  9301  uzss  9477  eluzp1m1  9480  infregelbex  9527  eluz2b2  9532  qre  9554  qaddcl  9564  qmulcl  9566  qreccl  9571  irradd  9575  irrmul  9576  elpqb  9578  cnref1o  9579  rprege0  9595  rprene0  9598  rpreap0  9599  rpcnne0  9600  rpcnap0  9601  rpregt0d  9630  rprege0d  9631  rprene0d  9632  rpcnne0d  9633  lediv2ad  9646  ledivge1le  9653  lediv12ad  9683  nnledivrp  9693  nn0ledivnn  9694  xrlttri3  9724  xrrebnd  9746  xrrege0  9752  xnn0xadd0  9794  xlesubadd  9810  elioo4g  9861  ioomax  9875  iccmax  9876  divelunit  9929  elfz5  9943  uzsubsubfz  9972  fzopth  9986  fzass4  9987  fzrev2  10010  uzsplit  10017  elfz2nn0  10037  difelfzle  10059  1fv  10064  4fvwrd4  10065  fzo1fzo0n0  10108  elfzom1elp1fzo  10127  subfzo0  10167  qtri3or  10168  adddivflid  10217  flltdivnn0lt  10229  intfracq  10245  modqid2  10276  modfzo0difsn  10320  seq3val  10383  seqvalcd  10384  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemab  10414  iseqf1olemmo  10417  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  expclzaplem  10469  leexp1a  10500  expubnd  10502  le2sq2  10520  sumsqeq0  10523  bernneq  10564  expnlbnd  10568  nn0opthd  10624  faclbnd6  10646  facavg  10648  seq3coll  10741  shftlem  10744  shftfvalg  10746  shftfval  10749  cvg1nlemcau  10912  cvg1nlemres  10913  rexuz3  10918  resqrexlemcvg  10947  resqrexlemglsq  10950  resqrexlemga  10951  sqrtle  10964  sqrtlt  10965  sqrt11  10967  sqrtsq2  10971  absmul  10997  sqabs  11010  abslt  11016  absle  11017  lenegsq  11023  maxleastb  11142  maxltsup  11146  rexanre  11148  negfi  11155  xrmaxiflemab  11174  xrmaxiflemlub  11175  xrmaxltsup  11185  xrmaxadd  11188  climcn2  11236  mulcn2  11239  summodclem2a  11308  summodc  11310  fsum3  11314  fsum3cvg3  11323  fsumcl2lem  11325  fsumadd  11333  fsump1i  11360  fsum0diaglem  11367  mptfzshft  11369  fsumrev  11370  fsummulc2  11375  fsum00  11389  expcnvap0  11429  mertenslemi1  11462  ntrivcvgap0  11476  prodmodclem3  11502  prodmodclem2a  11503  zproddc  11506  fprodseq  11510  fprodrev  11546  fprodconst  11547  eftlub  11617  efieq  11662  sincos1sgn  11691  demoivreALT  11700  dvdsval3  11717  dvdscmul  11744  dvdsmulc  11745  dvdscmulr  11746  dvdsmulcr  11747  modmulconst  11749  dvds2ln  11750  ltoddhalfle  11815  nn0o  11829  divalg2  11848  ndvdssub  11852  ndvdsadd  11853  infssuzex  11867  divgcdz  11889  gcd0id  11897  gcdaddm  11902  bezoutlemstep  11915  bezoutlemmain  11916  dfgcd3  11928  dfgcd2  11932  lcmcllem  11978  dvdslcm  11980  lcmgcdlem  11988  lcmgcdnn  11993  qredeq  12007  qredeu  12008  rpdvds  12010  divgcdcoprm0  12012  cncongr1  12014  cncongr2  12015  cncongrcoprm  12017  prmind2  12031  isprm6  12056  prmexpb  12060  cncongrprm  12066  sqrt2irrlem  12070  pw2dvdslemn  12074  oddpwdclemxy  12078  oddpwdclemdc  12082  oddpwdc  12083  hashdvds  12130  prmdiv  12144  hashgcdlem  12147  nnoddn2prmb  12171  pythagtriplem6  12179  pythagtriplem7  12180  pcpre1  12201  pccl  12208  pcmul  12210  pcdiv  12211  pcqmul  12212  pcqcl  12215  pcdvds  12223  pcndvds  12225  pcndvds2  12227  pc2dvds  12238  dvdsprmpweqle  12245  difsqpwdvds  12246  pcaddlem  12247  pcadd  12248  pcmptcl  12249  pcmpt  12250  fldivp1  12255  pcfac  12257  oddprmdvds  12261  ennnfonelemfun  12287  ennnfonelemim  12294  ctinfomlemom  12297  ctinfom  12298  ctinf  12300  ctiunctlemfo  12309  omctfn  12313  topgele  12568  tgcl  12605  epttop  12631  opnssneib  12697  iscnp4  12759  cnco  12762  cncnp  12771  cnrest2  12777  lmss  12787  txcnp  12812  txcn  12816  cnmpt12  12828  cnmpt22  12835  hmeof1o  12850  psmetres2  12874  distspace  12876  ismeti  12887  isxmetd  12888  xmetpsmet  12910  xblss2ps  12945  xblss2  12946  blcntrps  12956  blcntr  12957  blin2  12973  mopni3  13025  metequiv2  13037  bdmet  13043  xmettx  13051  cnbl0  13075  cnblcld  13076  tgioo  13087  elcncf1di  13107  dedekindeulemlu  13140  suplociccex  13144  dedekindicclemlu  13149  dedekindicc  13152  ivthinclemlopn  13155  ivthdec  13163  cnplimcim  13177  limccnp2lem  13186  dvfvalap  13191  reeff1olem  13233  sin0pilem1  13243  pilem3  13245  ptolemy  13286  sincosq1sgn  13288  sinq12gt0  13292  ioocosf1o  13316  rprelogbmulexp  13415  bj-nnan  13454  bj-charfun  13524  bdop  13592  bdunexb  13637  bj-om  13654  findset  13662  bj-peano4  13672  bj-inf2vn  13691  bj-inf2vn2  13692  pwle2  13712  pwf1oexmid  13713  sbthom  13739  qdencn  13740  trilpolemlt1  13754