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  5872  fnfvima  5889  resfvresima  5891  fcof1o  5930  isocnv  5952  isotr  5957  riotaprop  5997  acexmidlemcase  6013  caovlem2d  6215  f1ocnvd  6225  caofcom  6266  resfunexgALT  6270  elxp7  6333  2ndrn  6346  1stconst  6386  2ndconst  6387  cnvf1olem  6389  poxp  6397  dftpos4  6429  dfsmo2  6453  tfrlem5  6480  tfrlemiex  6497  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfr1onlemex  6513  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcllemex  6526  tfrcllemres  6528  tfrcl  6530  frecabex  6564  frecabcl  6565  frecfcllem  6570  frecrdg  6574  oawordi  6637  nntri3  6665  nntr2  6671  nnmordi  6684  iserd  6728  relelec  6744  erth  6748  qliftfun  6786  mapsncnv  6864  mptelixpg  6903  bren  6917  pw2f1odclem  7020  findcard2d  7080  findcard2sd  7081  isinfinf  7086  tridc  7089  nnwetri  7108  undifdcss  7115  fiintim  7123  fisseneq  7127  fidcenumlemim  7151  sbthlemi9  7164  supisolem  7207  ordiso2  7234  updjud  7281  difinfsn  7299  ctssdccl  7310  nnnninfeq  7327  omniwomnimkv  7366  pr2cv  7402  acfun  7422  exmidontriimlem2  7437  onntri45  7459  dftap2  7470  netap  7473  2omotaplemap  7476  ccfunen  7483  cc4f  7488  cc4n  7490  elni2  7534  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enqdc1  7582  addcmpblnq  7587  addclnq  7595  nqpi  7598  addassnqg  7602  mulassnqg  7604  mulcanenq  7605  distrnqg  7607  1qec  7608  recexnq  7610  subhalfnqq  7634  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  mulcanenq0ec  7665  nnnq0lem1  7666  addclnq0  7671  distrnq0  7679  addassnq0lemcl  7681  elnp1st2nd  7696  prarloc  7723  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  addclpr  7757  nqprm  7762  mullocprlem  7790  mullocpr  7791  mulclpr  7792  ltpopr  7815  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemrnd  7825  ltexprlemdisj  7826  addcanprleml  7834  addcanprlemu  7835  addcanprg  7836  recexprlemm  7844  recexprlemopl  7845  recexprlemopu  7847  recexprlemrnd  7849  recexprlemdisj  7850  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemrnd  7870  cauappcvgprlemdisj  7871  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemrnd  7893  caucvgprlemlim  7901  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemm  7916  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemrnd  7921  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  prsrlem1  7962  mulclsr  7974  mulasssrg  7978  distrsrg  7979  suplocsrlemb  8026  elreal2  8050  axmulass  8093  axdistr  8094  axcaucvglemcau  8118  add20  8654  mullt0  8660  rereim  8766  ltmul1  8772  cru  8782  mulap0r  8795  aprcl  8826  aptap  8830  divmuldivap  8892  divmuleqap  8897  divadddivap  8907  divmuldivapd  9012  divmuleqapd  9013  div2subap  9017  ltmul12a  9040  lemul12a  9042  lemulge11  9046  lediv12a  9074  lediv2a  9075  recgt1i  9078  recreclt  9080  ledivp1  9083  lemul1ad  9119  lemul2ad  9120  ltmul12ad  9121  lemul12ad  9122  lemul12bd  9123  nndivre  9179  nndivtr  9185  halfaddsubcl  9377  halfaddsub  9378  lt2halves  9380  nnrecl  9400  elnn0nn  9444  elnnnn0b  9446  elnnnn0c  9447  nn0addge1  9448  nn0addge2  9449  xnn0xrnemnf  9477  elnn0z  9492  elnnz1  9502  nzadd  9532  elz2  9551  zdivadd  9569  zdivmul  9570  zextle  9571  peano2uz2  9587  uzind  9591  btwnz  9599  uzss  9777  eluzp1m1  9780  infregelbex  9832  eluz2b2  9837  qre  9859  qaddcl  9869  qmulcl  9871  qreccl  9876  irradd  9880  irrmul  9881  elpqb  9884  cnref1o  9885  rprege0  9903  rprene0  9906  rpreap0  9907  rpcnne0  9908  rpcnap0  9909  rpregt0d  9938  rprege0d  9939  rprene0d  9940  rpcnne0d  9941  lediv2ad  9954  ledivge1le  9961  lediv12ad  9991  nnledivrp  10001  nn0ledivnn  10002  xrlttri3  10032  xrrebnd  10054  xrrege0  10060  xnn0xadd0  10102  xlesubadd  10118  elioo4g  10169  ioomax  10183  iccmax  10184  divelunit  10237  elfz5  10252  uzsubsubfz  10282  fzopth  10296  fzass4  10297  fzrev2  10320  uzsplit  10327  elfz2nn0  10347  difelfzle  10369  1fv  10374  4fvwrd4  10375  fzo1fzo0n0  10423  elfzom1elp1fzo  10448  subfzo0  10489  infssuzex  10494  qtri3or  10501  adddivflid  10553  flltdivnn0lt  10565  intfracq  10583  modqid2  10614  modfzo0difsn  10658  seq3val  10723  seqvalcd  10724  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seqf1oglem1  10782  seqf1oglem2  10783  expclzaplem  10826  leexp1a  10857  expubnd  10859  le2sq2  10878  sumsqeq0  10881  bernneq  10923  expnlbnd  10927  nn0opthd  10985  faclbnd6  11007  facavg  11009  seq3coll  11107  hash2en  11108  wrdnval  11148  ccat0  11177  ccatsymb  11183  ccatalpha  11194  swrdspsleq  11252  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  wrd2ind  11308  pfxccatin12lem2a  11312  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  swrdccatin1d  11328  swrdccatin2d  11329  shftlem  11381  shftfvalg  11383  shftfval  11386  cvg1nlemcau  11549  cvg1nlemres  11550  rexuz3  11555  resqrexlemcvg  11584  resqrexlemglsq  11587  resqrexlemga  11588  sqrtle  11601  sqrtlt  11602  sqrt11  11604  sqrtsq2  11608  absmul  11634  sqabs  11647  abslt  11653  absle  11654  lenegsq  11660  maxleastb  11779  maxltsup  11783  rexanre  11785  negfi  11793  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxltsup  11823  xrmaxadd  11826  climcn2  11874  mulcn2  11877  summodclem2a  11947  summodc  11949  fsum3  11953  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  fsump1i  11999  fsum0diaglem  12006  mptfzshft  12008  fsumrev  12009  fsummulc2  12014  fsum00  12028  expcnvap0  12068  mertenslemi1  12101  ntrivcvgap0  12115  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodrev  12185  fprodconst  12186  eftlub  12256  efieq  12301  sincos1sgn  12331  demoivreALT  12340  dvdsval3  12357  dvdscmul  12384  dvdsmulc  12385  dvdscmulr  12386  dvdsmulcr  12387  modmulconst  12389  dvds2ln  12390  ltoddhalfle  12459  nn0o  12473  divalg2  12492  ndvdssub  12496  ndvdsadd  12497  divgcdz  12547  gcd0id  12555  gcdaddm  12560  bezoutlemstep  12573  bezoutlemmain  12574  dfgcd3  12586  dfgcd2  12590  lcmcllem  12644  dvdslcm  12646  lcmgcdlem  12654  lcmgcdnn  12659  qredeq  12673  qredeu  12674  rpdvds  12676  divgcdcoprm0  12678  cncongr1  12680  cncongr2  12681  cncongrcoprm  12683  prmind2  12697  isprm5  12719  isprm6  12724  prmexpb  12728  cncongrprm  12734  sqrt2irrlem  12738  pw2dvdslemn  12742  oddpwdclemxy  12746  oddpwdclemdc  12750  oddpwdc  12751  hashdvds  12798  prmdiv  12812  hashgcdlem  12815  nnoddn2prmb  12840  pythagtriplem6  12848  pythagtriplem7  12849  pcpre1  12870  pccl  12877  pcmul  12879  pcdiv  12880  pcqmul  12881  pcqcl  12884  pcdvds  12893  pcndvds  12895  pcndvds2  12897  pc2dvds  12908  dvdsprmpweqle  12915  difsqpwdvds  12916  pcaddlem  12917  pcadd  12918  pcmptcl  12920  pcmpt  12921  fldivp1  12926  pcfac  12928  oddprmdvds  12932  infpnlem2  12938  4sqlem5  12960  4sqlem6  12961  4sqlem4a  12969  4sqexercise1  12976  4sqexercise2  12977  4sqlem13m  12981  4sqlem15  12983  4sqlem16  12984  ennnfonelemfun  13043  ennnfonelemim  13050  ctinfomlemom  13053  ctinfom  13054  ctinf  13056  ctiunctlemfo  13065  omctfn  13069  fnpr2ob  13428  ismgmid2  13468  fngsum  13476  igsumvalx  13477  gsumfzval  13479  gsum0g  13484  gsumval2  13485  issgrpd  13500  ismndd  13525  prdsidlem  13535  imasmnd2  13540  mhmf1o  13558  subsubm  13571  dfgrp2  13615  isgrpid2  13628  isgrpinv  13642  grplrinv  13645  dfgrp3mlem  13686  dfgrp3m  13687  dfgrp3me  13688  prdsinvlem  13696  imasgrp2  13702  mhmmnd  13708  issubg2m  13781  issubgrpd2  13782  grpissubg  13786  subsubg  13789  subgintm  13790  isnsg3  13799  nmzsubg  13802  eqgval  13815  eqgen  13819  isghmd  13844  ghmrn  13849  ghmpreima  13858  ghmf1o  13867  conjghm  13868  conjnmzb  13872  ghmpropd  13875  rinvmod  13901  imasabl  13928  rnglz  13964  isrngd  13972  srgdilem  13988  srglmhm  14012  srgrmhm  14013  ringdilem  14031  isringd  14060  ringsrg  14066  ringinvnzdiv  14069  imasring  14083  dvdsrd  14114  unitgrp  14136  isrim0  14181  isrhm2d  14185  rhmf1o  14188  rhmco  14194  rhmopp  14196  issubrng2  14230  subsubrng  14234  subrgugrp  14260  issubrg2  14261  subsubrg  14265  resrhm  14268  aprap  14306  lmodfopnelem2  14345  lsssubg  14397  islss3  14399  islss4  14402  lspsnel6  14428  lidlacl  14504  lidlsubg  14506  lidlrsppropdg  14515  2idlelbas  14536  cnfld1  14592  cnsubglem  14599  mulgghm2  14628  zndvds  14669  mplsubgfi  14721  topgele  14759  tgcl  14794  epttop  14820  opnssneib  14886  iscnp4  14948  cnco  14951  cncnp  14960  cnrest2  14966  lmss  14976  txcnp  15001  txcn  15005  cnmpt12  15017  cnmpt22  15024  hmeof1o  15039  psmetres2  15063  distspace  15065  ismeti  15076  isxmetd  15077  xmetpsmet  15099  xblss2ps  15134  xblss2  15135  blcntrps  15145  blcntr  15146  blin2  15162  mopni3  15214  metequiv2  15226  bdmet  15232  xmettx  15240  cnbl0  15264  cnblcld  15265  tgioo  15284  elcncf1di  15309  dedekindeulemlu  15351  suplociccex  15355  dedekindicclemlu  15360  dedekindicc  15363  ivthinclemlopn  15366  ivthdec  15374  ivthreinc  15375  ivthdichlem  15381  cnplimcim  15397  limccnp2lem  15406  dvfvalap  15411  plymullem  15480  reeff1olem  15501  sin0pilem1  15511  pilem3  15513  ptolemy  15554  sincosq1sgn  15556  sinq12gt0  15560  ioocosf1o  15584  rprelogbmulexp  15686  perfectlem2  15730  lgslem3  15737  lgsne0  15773  gausslemma2dlem0b  15785  gausslemma2dlem0c  15786  lgsquadlem2  15813  lgsquad2lem2  15817  2lgsoddprmlem2  15841  2sqlem8  15858  gropd  15904  grstructd2dom  15905  incistruhgr  15947  umgrislfupgrenlem  15987  umgrislfupgrdom  15988  uspgrupgrushgr  16039  usgrumgruspgr  16042  usgruspgrben  16043  usgrislfuspgrdom  16047  umgrvad2edg  16068  umgr2edgneu  16069  ushgredgedg  16083  ushgredgedgloop  16085  subgrprop3  16119  iswlkg  16186  wlk2f  16208  upgriswlkdc  16217  wlkv0  16226  wlklenvclwlk  16230  wlkepvtx  16232  upgr2wlkdc  16234  wlkres  16236  clwwlkccatlem  16257  clwwlkccat  16258  clwwlknbp  16272  clwwlknp  16274  clwwlkext2edg  16279  clwwlknon  16286  clwwlknonccat  16290  clwwlknonex2  16296  clwwlknonex2e  16297  trlsegvdeglem1  16317  bj-nnan  16358  bj-charfun  16428  bdop  16496  bdunexb  16541  bj-om  16558  findset  16566  bj-peano4  16576  bj-inf2vn  16595  bj-inf2vn2  16596  pwle2  16625  pwf1oexmid  16626  nnnninfex  16650  sbthom  16656  qdencn  16657  trilpolemlt1  16671  gfsumval  16707  gfsump1  16713