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	|- ( ph -> ps )
jca.2	|- ( ph -> ch )

Assertion

Ref	Expression
jca	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 |- ( ph -> ps )
2		jca.2	. 2 |- ( ph -> ch )
3		pm3.2 139	. 2 |- ( ps -> ( ch -> ( ps /\ ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps /\ ch ) )

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  biadanid  614  ioran  753  ordi  817  stdcndc  846  stdcndcOLD  847  dfandc  885  mpbi2and  945  mpbir2and  946  pm4.82  952  pm4.83dc  953  rnlem  978  syl22anc  1250  syl112anc  1253  syl121anc  1254  syl211anc  1255  syl23anc  1256  syl32anc  1257  syl122anc  1258  syl212anc  1259  syl221anc  1260  syl222anc  1265  syl123anc  1266  syl132anc  1267  syl213anc  1268  syl231anc  1269  syl312anc  1270  syl321anc  1271  syl223anc  1275  syl232anc  1276  syl322anc  1277  syl233anc  1278  syl323anc  1279  syl332anc  1280  ecased  1360  19.26  1492  nfand  1579  19.40  1642  equsexd  1740  sbcof2  1821  sbequ8  1858  eu2  2086  eu3h  2087  eu5  2089  mooran2  2115  datisi  2152  felapton  2156  darapti  2157  dimatis  2159  fresison  2160  fesapo  2162  reximssdv  2598  r19.26  2620  r19.29af2  2634  r19.40  2648  eqvinc  2884  eqvincg  2885  elrabd  2919  reu6  2950  reu3  2951  indifdir  3416  undif3ss  3421  un00  3494  eqifdc  3593  disjpr2  3683  prel12  3798  prneimg  3801  preqsn  3802  disjiun  4025  opth  4267  0nelop  4278  euotd  4284  opelopabsb  4291  ispod  4336  elon2  4408  unexb  4474  opeluu  4482  eusvnfb  4486  suc11g  4590  nlimsucg  4599  tfi  4615  vtoclr  4708  opthprc  4711  ideqg  4814  resiexg  4988  dminss  5081  imainss  5082  ssxpbm  5102  relrelss  5193  funopg  5289  fntpg  5311  fun11uni  5325  imain  5337  funimaexglem  5338  funssxp  5424  ffdm  5425  f00  5446  dffo2  5481  fodmrnu  5485  foco  5488  fun11iun  5522  f1o00  5536  fsnd  5544  fv3  5578  dff2  5703  dff3im  5704  dffo4  5707  ffnfv  5717  ffvresb  5722  fsn2  5733  fconstfvm  5777  fnfvima  5794  fcof1o  5833  isocnv  5855  isotr  5860  riotaprop  5898  acexmidlemcase  5914  caovlem2d  6113  f1ocnvd  6122  caofcom  6158  resfunexgALT  6162  elxp7  6225  2ndrn  6238  1stconst  6276  2ndconst  6277  cnvf1olem  6279  poxp  6287  dftpos4  6318  dfsmo2  6342  tfrlem5  6369  tfrlemiex  6386  tfr1onlemsucaccv  6396  tfr1onlembfn  6399  tfr1onlemex  6402  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllembfn  6412  tfrcllemex  6415  tfrcllemres  6417  tfrcl  6419  frecabex  6453  frecabcl  6454  frecfcllem  6459  frecrdg  6463  oawordi  6524  nntri3  6552  nntr2  6558  nnmordi  6571  iserd  6615  relelec  6631  erth  6635  qliftfun  6673  mapsncnv  6751  mptelixpg  6790  bren  6803  pw2f1odclem  6892  findcard2d  6949  findcard2sd  6950  isinfinf  6955  tridc  6957  nnwetri  6974  undifdcss  6981  fiintim  6987  fisseneq  6990  fidcenumlemim  7013  sbthlemi9  7026  supisolem  7069  ordiso2  7096  updjud  7143  difinfsn  7161  ctssdccl  7172  nnnninfeq  7189  omniwomnimkv  7228  acfun  7269  exmidontriimlem2  7284  onntri45  7303  dftap2  7313  netap  7316  2omotaplemap  7319  ccfunen  7326  cc4f  7331  cc4n  7333  elni2  7376  dfplpq2  7416  dfmpq2  7417  enqbreq2  7419  enqdc1  7424  addcmpblnq  7429  addclnq  7437  nqpi  7440  addassnqg  7444  mulassnqg  7446  mulcanenq  7447  distrnqg  7449  1qec  7450  recexnq  7452  subhalfnqq  7476  enq0tr  7496  nqnq0pi  7500  nq0nn  7504  mulcanenq0ec  7507  nnnq0lem1  7508  addclnq0  7513  distrnq0  7521  addassnq0lemcl  7523  elnp1st2nd  7538  prarloc  7565  addlocprlemlt  7593  addlocprlemeq  7595  addlocprlemgt  7596  addclpr  7599  nqprm  7604  mullocprlem  7632  mullocpr  7633  mulclpr  7634  ltpopr  7657  ltaddpr  7659  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemrnd  7667  ltexprlemdisj  7668  addcanprleml  7676  addcanprlemu  7677  addcanprg  7678  recexprlemm  7686  recexprlemopl  7687  recexprlemopu  7689  recexprlemrnd  7691  recexprlemdisj  7692  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemrnd  7712  cauappcvgprlemdisj  7713  cauappcvgprlemlim  7723  caucvgprlemnkj  7728  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemrnd  7735  caucvgprlemlim  7743  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnjltk  7753  caucvgprprlemm  7758  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemrnd  7763  caucvgprprlemexbt  7768  caucvgprprlemlim  7773  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  prsrlem1  7804  mulclsr  7816  mulasssrg  7820  distrsrg  7821  suplocsrlemb  7868  elreal2  7892  axmulass  7935  axdistr  7936  axcaucvglemcau  7960  add20  8495  mullt0  8501  rereim  8607  ltmul1  8613  cru  8623  mulap0r  8636  aprcl  8667  aptap  8671  divmuldivap  8733  divmuleqap  8738  divadddivap  8748  divmuldivapd  8853  divmuleqapd  8854  div2subap  8858  ltmul12a  8881  lemul12a  8883  lemulge11  8887  lediv12a  8915  lediv2a  8916  recgt1i  8919  recreclt  8921  ledivp1  8924  lemul1ad  8960  lemul2ad  8961  ltmul12ad  8962  lemul12ad  8963  lemul12bd  8964  nndivre  9020  nndivtr  9026  halfaddsubcl  9218  halfaddsub  9219  lt2halves  9221  nnrecl  9241  elnn0nn  9285  elnnnn0b  9287  elnnnn0c  9288  nn0addge1  9289  nn0addge2  9290  xnn0xrnemnf  9318  elnn0z  9333  elnnz1  9343  nzadd  9372  elz2  9391  zdivadd  9409  zdivmul  9410  zextle  9411  peano2uz2  9427  uzind  9431  btwnz  9439  uzss  9616  eluzp1m1  9619  infregelbex  9666  eluz2b2  9671  qre  9693  qaddcl  9703  qmulcl  9705  qreccl  9710  irradd  9714  irrmul  9715  elpqb  9718  cnref1o  9719  rprege0  9737  rprene0  9740  rpreap0  9741  rpcnne0  9742  rpcnap0  9743  rpregt0d  9772  rprege0d  9773  rprene0d  9774  rpcnne0d  9775  lediv2ad  9788  ledivge1le  9795  lediv12ad  9825  nnledivrp  9835  nn0ledivnn  9836  xrlttri3  9866  xrrebnd  9888  xrrege0  9894  xnn0xadd0  9936  xlesubadd  9952  elioo4g  10003  ioomax  10017  iccmax  10018  divelunit  10071  elfz5  10086  uzsubsubfz  10116  fzopth  10130  fzass4  10131  fzrev2  10154  uzsplit  10161  elfz2nn0  10181  difelfzle  10203  1fv  10208  4fvwrd4  10209  fzo1fzo0n0  10253  elfzom1elp1fzo  10272  subfzo0  10312  qtri3or  10313  adddivflid  10364  flltdivnn0lt  10376  intfracq  10394  modqid2  10425  modfzo0difsn  10469  seq3val  10534  seqvalcd  10535  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemmo  10579  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seqf1oglem1  10593  seqf1oglem2  10594  expclzaplem  10637  leexp1a  10668  expubnd  10670  le2sq2  10689  sumsqeq0  10692  bernneq  10734  expnlbnd  10738  nn0opthd  10796  faclbnd6  10818  facavg  10820  seq3coll  10916  wrdnval  10947  shftlem  10963  shftfvalg  10965  shftfval  10968  cvg1nlemcau  11131  cvg1nlemres  11132  rexuz3  11137  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  sqrtle  11183  sqrtlt  11184  sqrt11  11186  sqrtsq2  11190  absmul  11216  sqabs  11229  abslt  11235  absle  11236  lenegsq  11242  maxleastb  11361  maxltsup  11365  rexanre  11367  negfi  11374  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxltsup  11404  xrmaxadd  11407  climcn2  11455  mulcn2  11458  summodclem2a  11527  summodc  11529  fsum3  11533  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  fsump1i  11579  fsum0diaglem  11586  mptfzshft  11588  fsumrev  11589  fsummulc2  11594  fsum00  11608  expcnvap0  11648  mertenslemi1  11681  ntrivcvgap0  11695  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodrev  11765  fprodconst  11766  eftlub  11836  efieq  11881  sincos1sgn  11911  demoivreALT  11920  dvdsval3  11937  dvdscmul  11964  dvdsmulc  11965  dvdscmulr  11966  dvdsmulcr  11967  modmulconst  11969  dvds2ln  11970  ltoddhalfle  12037  nn0o  12051  divalg2  12070  ndvdssub  12074  ndvdsadd  12075  infssuzex  12089  divgcdz  12111  gcd0id  12119  gcdaddm  12124  bezoutlemstep  12137  bezoutlemmain  12138  dfgcd3  12150  dfgcd2  12154  lcmcllem  12208  dvdslcm  12210  lcmgcdlem  12218  lcmgcdnn  12223  qredeq  12237  qredeu  12238  rpdvds  12240  divgcdcoprm0  12242  cncongr1  12244  cncongr2  12245  cncongrcoprm  12247  prmind2  12261  isprm5  12283  isprm6  12288  prmexpb  12292  cncongrprm  12298  sqrt2irrlem  12302  pw2dvdslemn  12306  oddpwdclemxy  12310  oddpwdclemdc  12314  oddpwdc  12315  hashdvds  12362  prmdiv  12376  hashgcdlem  12379  nnoddn2prmb  12403  pythagtriplem6  12411  pythagtriplem7  12412  pcpre1  12433  pccl  12440  pcmul  12442  pcdiv  12443  pcqmul  12444  pcqcl  12447  pcdvds  12456  pcndvds  12458  pcndvds2  12460  pc2dvds  12471  dvdsprmpweqle  12478  difsqpwdvds  12479  pcaddlem  12480  pcadd  12481  pcmptcl  12483  pcmpt  12484  fldivp1  12489  pcfac  12491  oddprmdvds  12495  infpnlem2  12501  4sqlem5  12523  4sqlem6  12524  4sqlem4a  12532  4sqexercise1  12539  4sqexercise2  12540  4sqlem13m  12544  4sqlem15  12546  4sqlem16  12547  ennnfonelemfun  12577  ennnfonelemim  12584  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  ctiunctlemfo  12599  omctfn  12603  fnpr2ob  12926  ismgmid2  12966  fngsum  12974  igsumvalx  12975  gsumfzval  12977  gsum0g  12982  gsumval2  12983  issgrpd  12998  ismndd  13021  mhmf1o  13045  subsubm  13058  dfgrp2  13102  isgrpid2  13115  isgrpinv  13129  grplrinv  13132  dfgrp3mlem  13173  dfgrp3m  13174  dfgrp3me  13175  imasgrp2  13183  mhmmnd  13189  issubg2m  13262  issubgrpd2  13263  grpissubg  13267  subsubg  13270  subgintm  13271  isnsg3  13280  nmzsubg  13283  eqgval  13296  eqgen  13300  isghmd  13325  ghmrn  13330  ghmpreima  13339  ghmf1o  13348  conjghm  13349  conjnmzb  13353  ghmpropd  13356  rinvmod  13382  imasabl  13409  rnglz  13444  isrngd  13452  srgdilem  13468  srglmhm  13492  srgrmhm  13493  ringdilem  13511  isringd  13540  ringsrg  13546  ringinvnzdiv  13549  imasring  13563  dvdsrd  13593  unitgrp  13615  isrim0  13660  isrhm2d  13664  rhmf1o  13667  rhmco  13673  rhmopp  13675  issubrng2  13709  subsubrng  13713  subrgugrp  13739  issubrg2  13740  subsubrg  13744  resrhm  13747  aprap  13785  lmodfopnelem2  13824  lsssubg  13876  islss3  13878  islss4  13881  lspsnel6  13907  lidlacl  13983  lidlsubg  13985  lidlrsppropdg  13994  2idlelbas  14015  cnfld1  14071  cnsubglem  14078  mulgghm2  14107  zndvds  14148  topgele  14208  tgcl  14243  epttop  14269  opnssneib  14335  iscnp4  14397  cnco  14400  cncnp  14409  cnrest2  14415  lmss  14425  txcnp  14450  txcn  14454  cnmpt12  14466  cnmpt22  14473  hmeof1o  14488  psmetres2  14512  distspace  14514  ismeti  14525  isxmetd  14526  xmetpsmet  14548  xblss2ps  14583  xblss2  14584  blcntrps  14594  blcntr  14595  blin2  14611  mopni3  14663  metequiv2  14675  bdmet  14681  xmettx  14689  cnbl0  14713  cnblcld  14714  tgioo  14733  elcncf1di  14758  dedekindeulemlu  14800  suplociccex  14804  dedekindicclemlu  14809  dedekindicc  14812  ivthinclemlopn  14815  ivthdec  14823  ivthreinc  14824  ivthdichlem  14830  cnplimcim  14846  limccnp2lem  14855  dvfvalap  14860  plymullem  14929  reeff1olem  14947  sin0pilem1  14957  pilem3  14959  ptolemy  15000  sincosq1sgn  15002  sinq12gt0  15006  ioocosf1o  15030  rprelogbmulexp  15129  lgslem3  15159  lgsne0  15195  gausslemma2dlem0b  15207  gausslemma2dlem0c  15208  lgsquadlem2  15235  lgsquad2lem2  15239  2lgsoddprmlem2  15263  2sqlem8  15280  bj-nnan  15298  bj-charfun  15369  bdop  15437  bdunexb  15482  bj-om  15499  findset  15507  bj-peano4  15517  bj-inf2vn  15536  bj-inf2vn2  15537  pwle2  15559  pwf1oexmid  15560  sbthom  15586  qdencn  15587  trilpolemlt1  15601