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  421  jcab  611  biadanid  622  ioran  764  ordi  828  stdcndc  857  stdcndcOLD  858  dfandc  896  mpbi2and  956  mpbir2and  957  pm4.82  963  pm4.83dc  964  rnlem  989  ifp2  993  syl22anc  1279  syl112anc  1282  syl121anc  1283  syl211anc  1284  syl23anc  1285  syl32anc  1286  syl122anc  1287  syl212anc  1288  syl221anc  1289  syl222anc  1294  syl123anc  1295  syl132anc  1296  syl213anc  1297  syl231anc  1298  syl312anc  1299  syl321anc  1300  syl223anc  1304  syl232anc  1305  syl322anc  1306  syl233anc  1307  syl323anc  1308  syl332anc  1309  ecased  1390  19.26  1534  nfand  1621  19.40  1684  equsexd  1782  sbcof2  1863  sbequ8  1900  eu2  2131  eu3h  2132  eu5  2134  mooran2  2160  datisi  2197  felapton  2201  darapti  2202  dimatis  2204  fresison  2205  fesapo  2207  reximssdv  2654  r19.26  2677  r19.29af2  2691  r19.40  2705  eqvinc  2949  eqvincg  2950  elrabd  2984  reu6  3015  reu3  3016  indifdir  3487  undif3ss  3492  un00  3566  vvin  3568  eqifdc  3674  disjpr2  3769  prel12  3891  prneimg  3894  preqsn  3895  disjiun  4120  opth  4372  0nelop  4383  euotd  4390  opelopabsb  4397  ispod  4444  elon2  4516  unexb  4583  opeluu  4591  eusvnfb  4595  suc11g  4699  nlimsucg  4708  tfi  4724  vtoclr  4818  opthprc  4821  ideqg  4926  resiexg  5103  dminss  5197  imainss  5198  ssxpbm  5218  relrelss  5309  funopg  5406  fununfun  5419  fntpg  5432  fun11uni  5446  imain  5458  funimaexglem  5459  funssxp  5552  ffdm  5553  f00  5579  dffo2  5614  fodmrnu  5618  foco  5621  fun11iun  5655  f1o00  5671  fsnd  5679  fv3  5713  fvun1d  5765  fvun2d  5766  dff2  5843  dff3im  5844  dffo4  5847  ffnfv  5857  ffvresb  5862  fsn2  5873  fconstfvm  5924  fnfvima  5943  resfvresima  5946  fcof1o  5985  isocnv  6007  isotr  6012  riotaprop  6054  acexmidlemcase  6070  caovlem2d  6272  f1ocnvd  6282  f1o3d  6288  caofcom  6323  resfunexgALT  6327  elxp7  6394  2ndrn  6407  1stconst  6447  2ndconst  6448  cnvf1olem  6450  poxp  6458  ressuppss  6484  funsssuppss  6488  dftpos4  6524  dfsmo2  6548  tfrlem5  6575  tfrlemiex  6592  tfr1onlemsucaccv  6602  tfr1onlembfn  6605  tfr1onlemex  6608  tfr1onlemres  6610  tfrcllemsucaccv  6615  tfrcllembfn  6618  tfrcllemex  6621  tfrcllemres  6623  tfrcl  6625  frecabex  6659  frecabcl  6660  frecfcllem  6665  frecrdg  6669  oawordi  6732  nntri3  6760  nntr2  6766  nnmordi  6779  iserd  6823  relelec  6839  erth  6843  qliftfun  6881  mapsnd  6960  mapsncnv  6967  mptelixpg  7006  bren  7020  pw2f1odclem  7124  mapunen  7141  findcard2d  7185  findcard2sd  7186  isinfinf  7191  tridc  7194  nnwetri  7213  undifdcss  7220  fiintim  7228  fisseneq  7232  fidcenumlemim  7259  sbthlemi9  7272  supisolem  7338  ordiso2  7365  updjud  7412  difinfsn  7430  ctssdccl  7441  nnnninfeq  7458  omniwomnimkv  7497  pr2cv  7533  acfun  7553  exmidontriimlem2  7568  onntri45  7590  dftap2  7607  netap  7610  2omotaplemap  7613  ccfunen  7620  cc4f  7625  cc4n  7627  elni2  7671  dfplpq2  7711  dfmpq2  7712  enqbreq2  7714  enqdc1  7719  addcmpblnq  7724  addclnq  7732  nqpi  7735  addassnqg  7739  mulassnqg  7741  mulcanenq  7742  distrnqg  7744  1qec  7745  recexnq  7747  subhalfnqq  7771  enq0tr  7791  nqnq0pi  7795  nq0nn  7799  mulcanenq0ec  7802  nnnq0lem1  7803  addclnq0  7808  distrnq0  7816  addassnq0lemcl  7818  elnp1st2nd  7833  prarloc  7860  addlocprlemlt  7888  addlocprlemeq  7890  addlocprlemgt  7891  addclpr  7894  nqprm  7899  mullocprlem  7927  mullocpr  7928  mulclpr  7929  ltpopr  7952  ltaddpr  7954  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemrnd  7962  ltexprlemdisj  7963  addcanprleml  7971  addcanprlemu  7972  addcanprg  7973  recexprlemm  7981  recexprlemopl  7982  recexprlemopu  7984  recexprlemrnd  7986  recexprlemdisj  7987  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemrnd  8007  cauappcvgprlemdisj  8008  cauappcvgprlemlim  8018  caucvgprlemnkj  8023  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemrnd  8030  caucvgprlemlim  8038  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnjltk  8048  caucvgprprlemm  8053  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemrnd  8058  caucvgprprlemexbt  8063  caucvgprprlemlim  8068  suplocexprlemrl  8074  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  prsrlem1  8099  mulclsr  8111  mulasssrg  8115  distrsrg  8116  suplocsrlemb  8163  elreal2  8187  axmulass  8230  axdistr  8231  axcaucvglemcau  8255  add20  8792  mullt0  8798  rereim  8904  ltmul1  8910  cru  8920  mulap0r  8933  aprcl  8964  aptap  8968  divmuldivap  9032  divmuleqap  9037  divadddivap  9047  divmuldivapd  9152  divmuleqapd  9153  div2subap  9157  ltmul12a  9180  lemul12a  9182  lemulge11  9186  lediv12a  9214  lediv2a  9215  recgt1i  9218  recreclt  9220  ledivp1  9223  lemul1ad  9259  lemul2ad  9260  ltmul12ad  9261  lemul12ad  9262  lemul12bd  9263  nndivre  9319  nndivtr  9325  halfaddsubcl  9517  halfaddsub  9518  lt2halves  9520  nnrecl  9540  elnn0nn  9584  elnnnn0b  9586  elnnnn0c  9587  nn0addge1  9588  nn0addge2  9589  xnn0xrnemnf  9621  elnn0z  9636  elnnz1  9646  nzadd  9676  elz2  9695  zdivadd  9714  zdivmul  9715  zextle  9716  peano2uz2  9732  uzind  9736  btwnz  9744  uzss  9922  eluzp1m1  9925  infregelbex  9977  eluz2b2  9982  qre  10004  qaddcl  10014  qmulcl  10016  qreccl  10021  irradd  10025  irrmul  10026  elpqb  10029  cnref1o  10030  rprege0  10048  rprene0  10051  rpreap0  10052  rpcnne0  10053  rpcnap0  10054  rpregt0d  10083  rprege0d  10084  rprene0d  10085  rpcnne0d  10086  lediv2ad  10099  ledivge1le  10106  lediv12ad  10136  nnledivrp  10146  nn0ledivnn  10147  xrlttri3  10178  xrrebnd  10200  xrrege0  10206  xnn0xadd0  10248  xlesubadd  10264  elioo4g  10315  ioomax  10329  iccmax  10330  divelunit  10383  elfz5  10399  uzsubsubfz  10430  fzopth  10445  fzass4  10446  fzrev2  10470  uzsplit  10477  elfz2nn0  10497  difelfzle  10519  1fv  10524  4fvwrd4  10525  fzo1fzo0n0  10573  elfzom1elp1fzo  10598  subfzo0  10639  infssuzex  10644  infssfzcldc  10647  infssfzledc  10648  qtri3or  10653  adddivflid  10705  flltdivnn0lt  10717  intfracq  10735  modqid2  10766  modfzo0difsn  10810  seq3val  10875  seqvalcd  10876  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  iseqf1olemmo  10920  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seqf1oglem1  10934  seqf1oglem2  10935  expclzaplem  10978  leexp1a  11009  expubnd  11011  le2sq2  11030  sumsqeq0  11033  bernneq  11076  expnlbnd  11080  nn0opthd  11138  faclbnd6  11160  facavg  11162  sseqn  11257  hashfibclem  11260  hashf1lem2  11264  seq3coll  11272  hash2en  11273  wrdnval  11313  ccat0  11342  ccatsymb  11348  ccatalpha  11359  swrdspsleq  11417  pfxtrcfv  11443  pfxsuffeqwrdeq  11448  wrd2ind  11473  pfxccatin12lem2a  11477  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  pfxccatpfx1  11486  pfxccatpfx2  11487  swrdccatin1d  11493  swrdccatin2d  11494  shftlem  11559  shftfvalg  11561  shftfval  11564  cvg1nlemcau  11728  cvg1nlemres  11729  rexuz3  11734  resqrexlemcvg  11763  resqrexlemglsq  11766  resqrexlemga  11767  sqrtle  11780  sqrtlt  11781  sqrt11  11783  sqrtsq2  11787  absmul  11813  sqabs  11826  abslt  11832  absle  11833  lenegsq  11839  maxleastb  11958  maxltsup  11962  rexanre  11964  negfi  11972  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxltsup  12002  xrmaxadd  12005  climcn2  12053  mulcn2  12056  summodclem2a  12126  summodc  12128  fsum3  12132  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  fsump1i  12178  fsum0diaglem  12185  mptfzshft  12187  fsumrev  12188  fsummulc2  12193  fsum00  12207  expcnvap0  12247  mertenslemi1  12280  ntrivcvgap0  12294  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodrev  12364  fprodconst  12365  eftlub  12435  efieq  12480  sincos1sgn  12510  demoivreALT  12519  dvdsval3  12536  dvdscmul  12563  dvdsmulc  12564  dvdscmulr  12565  dvdsmulcr  12566  modmulconst  12568  dvds2ln  12569  ltoddhalfle  12638  nn0o  12652  divalg2  12671  ndvdssub  12675  ndvdsadd  12676  divgcdz  12726  gcd0id  12734  gcdaddm  12739  bezoutlemstep  12752  bezoutlemmain  12753  dfgcd3  12765  dfgcd2  12769  lcmcllem  12823  dvdslcm  12825  lcmgcdlem  12833  lcmgcdnn  12838  qredeq  12852  qredeu  12853  rpdvds  12855  divgcdcoprm0  12857  cncongr1  12859  cncongr2  12860  cncongrcoprm  12862  prmind2  12876  isprm5  12898  isprm6  12903  prmexpb  12907  cncongrprm  12913  sqrt2irrlem  12917  pw2dvdslemn  12921  oddpwdclemxy  12925  oddpwdclemdc  12929  oddpwdc  12930  hashdvds  12977  prmdiv  12991  hashgcdlem  12994  nnoddn2prmb  13019  pythagtriplem6  13027  pythagtriplem7  13028  pcpre1  13049  pccl  13056  pcmul  13058  pcdiv  13059  pcqmul  13060  pcqcl  13063  pcdvds  13072  pcndvds  13074  pcndvds2  13076  pc2dvds  13087  dvdsprmpweqle  13094  difsqpwdvds  13095  pcaddlem  13096  pcadd  13097  pcmptcl  13099  pcmpt  13100  fldivp1  13105  pcfac  13107  oddprmdvds  13111  infpnlem2  13117  4sqlem5  13139  4sqlem6  13140  4sqlem4a  13148  4sqexercise1  13155  4sqexercise2  13156  4sqlem13m  13160  4sqlem15  13162  4sqlem16  13163  ballotfilem2  13206  ballotfilemfp1  13209  ballotfilemsf1o  13235  ballotfilemrinv0  13254  ballotfilem7  13257  ballotfilemth  13259  ennnfonelemfun  13286  ennnfonelemim  13293  ctinfomlemom  13296  ctinfom  13297  ctinf  13299  ctiunctlemfo  13308  omctfn  13312  fnpr2ob  13638  ismgmid2  13677  fngzsum  13685  gzsumvalx  13686  gzsumfzval  13688  gzsum0  13690  gzsumval2  13691  issgrpd  13704  ismndd  13727  imasmnd2  13736  mhmf1o  13754  subsubm  13767  dfgrp2  13809  isgrpid2  13822  isgrpinv  13836  grplrinv  13839  dfgrp3mlem  13880  dfgrp3m  13881  dfgrp3me  13882  imasgrp2  13890  mhmmnd  13896  issubg2m  13969  issubgrpd2  13970  grpissubg  13974  subsubg  13977  subgintm  13978  isnsg3  13987  nmzsubg  13990  eqgval  14003  eqgen  14007  isghmd  14032  ghmrn  14037  ghmpreima  14046  ghmf1o  14055  conjghm  14056  conjnmzb  14060  ghmpropd  14063  rinvmod  14090  imasabl  14117  gsumvalfi  14129  gsump1  14134  prdsidlem  14170  prdsinvlem  14173  rnglz  14219  isrngd  14227  rng1zr  14234  srgdilem  14247  srg1zr  14265  srglmhm  14271  srgrmhm  14272  ringdilem  14290  isringd  14319  ringsrg  14325  ringinvnzdiv  14328  imasring  14342  dvdsrd  14374  unitgrp  14396  isrim0  14441  isrhm2d  14445  rhmf1o  14448  rhmco  14454  rhmopp  14456  issubrng2  14491  subsubrng  14495  subrgugrp  14521  issubrg2  14522  subsubrg  14526  resrhm  14529  ringunitap  14566  aprap  14571  drngunitap  14581  lmodfopnelem2  14634  lsssubg  14686  islss3  14688  islss4  14691  lspsnel6  14717  lidlacl  14793  lidlsubg  14795  lidlrsppropdg  14804  2idlelbas  14825  cnfld1  14881  cnsubglem  14888  mulgghm2  14915  zndvds  14956  psrbagcon  14985  mplsubgfi  15015  topgele  15053  tgcl  15088  epttop  15114  opnssneib  15180  iscnp4  15242  cnco  15245  cncnp  15254  cnrest2  15260  lmss  15270  txcnp  15295  txcn  15299  cnmpt12  15311  cnmpt22  15318  hmeof1o  15333  psmetres2  15357  distspace  15359  ismeti  15370  isxmetd  15371  xmetpsmet  15393  xblss2ps  15428  xblss2  15429  blcntrps  15439  blcntr  15440  blin2  15456  mopni3  15508  metequiv2  15520  bdmet  15526  xmettx  15534  cnbl0  15558  cnblcld  15559  tgioo  15578  elcncf1di  15603  dedekindeulemlu  15645  suplociccex  15649  dedekindicclemlu  15654  dedekindicc  15657  ivthinclemlopn  15660  ivthdec  15668  ivthreinc  15669  ivthdichlem  15675  cnplimcim  15691  limccnp2lem  15700  dvfvalap  15705  plymullem  15774  reeff1olem  15795  sin0pilem1  15805  pilem3  15807  ptolemy  15848  sincosq1sgn  15850  sinq12gt0  15854  ioocosf1o  15878  rprelogbmulexp  15981  pellexlem3  16007  perfectlem2  16028  lgslem3  16035  lgsne0  16071  gausslemma2dlem0b  16083  gausslemma2dlem0c  16084  lgsquadlem2  16111  lgsquad2lem2  16115  2lgsoddprmlem2  16139  2sqlem8  16156  gropd  16202  grstructd2dom  16203  incistruhgr  16245  umgrislfupgrenlem  16285  umgrislfupgrdom  16286  uspgrupgrushgr  16337  usgrumgruspgr  16340  usgruspgrben  16341  usgrislfuspgrdom  16345  umgrvad2edg  16366  umgr2edgneu  16367  ushgredgedg  16381  ushgredgedgloop  16383  subgrprop3  16417  iswlkg  16484  wlk2f  16506  upgriswlkdc  16515  wlkv0  16524  wlklenvclwlk  16528  wlkepvtx  16530  upgr2wlkdc  16532  wlkres  16534  clwwlkccatlem  16555  clwwlkccat  16556  clwwlknbp  16570  clwwlknp  16572  clwwlkext2edg  16577  clwwlknon  16584  clwwlknonccat  16588  clwwlknonex2  16594  clwwlknonex2e  16595  trlsegvdeglem1  16615  dichmul0orlem3  16669  bj-nnan  16678  bj-charfun  16747  bdop  16815  bdunexb  16860  bj-om  16877  findset  16885  bj-peano4  16895  bj-inf2vn  16914  bj-inf2vn2  16915  pwle2  16942  pwf1oexmid  16943  nnnninfex  16970  sbthom  16976  qdencn  16977  trilpolemlt1  16995