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  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  3567  vvin  3569  eqifdc  3677  disjpr2  3772  prel12  3894  prneimg  3897  preqsn  3898  disjiun  4123  opth  4375  0nelop  4386  euotd  4393  opelopabsb  4400  ispod  4447  elon2  4519  unexb  4586  opeluu  4594  eusvnfb  4598  suc11g  4702  nlimsucg  4711  tfi  4727  vtoclr  4821  opthprc  4824  ideqg  4929  resiexg  5106  dminss  5200  imainss  5201  ssxpbm  5221  relrelss  5312  funopg  5409  fununfun  5422  fntpg  5435  fun11uni  5449  imain  5461  funimaexglem  5462  funssxp  5555  ffdm  5556  f00  5582  dffo2  5617  fodmrnu  5621  foco  5624  fun11iun  5658  f1o00  5674  fsnd  5682  fv3  5716  fvun1d  5768  fvun2d  5769  dff2  5846  dff3im  5847  dffo4  5850  ffnfv  5860  ffvresb  5865  fsn2  5876  fconstfvm  5927  fnfvima  5946  resfvresima  5949  fcof1o  5988  isocnv  6010  isotr  6015  riotaprop  6057  acexmidlemcase  6073  caovlem2d  6275  f1ocnvd  6285  f1o3d  6291  caofcom  6326  resfunexgALT  6330  elxp7  6397  2ndrn  6410  1stconst  6450  2ndconst  6451  cnvf1olem  6453  poxp  6461  ressuppss  6487  funsssuppss  6491  dftpos4  6527  dfsmo2  6551  tfrlem5  6578  tfrlemiex  6595  tfr1onlemsucaccv  6605  tfr1onlembfn  6608  tfr1onlemex  6611  tfr1onlemres  6613  tfrcllemsucaccv  6618  tfrcllembfn  6621  tfrcllemex  6624  tfrcllemres  6626  tfrcl  6628  frecabex  6662  frecabcl  6663  frecfcllem  6668  frecrdg  6672  oawordi  6735  nntri3  6763  nntr2  6769  nnmordi  6782  iserd  6826  relelec  6842  erth  6846  qliftfun  6884  mapsnd  6963  mapsncnv  6970  mptelixpg  7009  bren  7023  pw2f1odclem  7127  mapunen  7144  findcard2d  7188  findcard2sd  7189  isinfinf  7194  tridc  7197  nnwetri  7216  undifdcss  7223  fiintim  7231  fisseneq  7235  fidcenumlemim  7262  sbthlemi9  7275  supisolem  7341  ordiso2  7368  updjud  7415  difinfsn  7433  ctssdccl  7444  nnnninfeq  7461  omniwomnimkv  7500  pr2cv  7536  acfun  7556  exmidontriimlem2  7571  onntri45  7593  dftap2  7610  netap  7613  2omotaplemap  7616  ccfunen  7623  cc4f  7628  cc4n  7630  elni2  7674  dfplpq2  7714  dfmpq2  7715  enqbreq2  7717  enqdc1  7722  addcmpblnq  7727  addclnq  7735  nqpi  7738  addassnqg  7742  mulassnqg  7744  mulcanenq  7745  distrnqg  7747  1qec  7748  recexnq  7750  subhalfnqq  7774  enq0tr  7794  nqnq0pi  7798  nq0nn  7802  mulcanenq0ec  7805  nnnq0lem1  7806  addclnq0  7811  distrnq0  7819  addassnq0lemcl  7821  elnp1st2nd  7836  prarloc  7863  addlocprlemlt  7891  addlocprlemeq  7893  addlocprlemgt  7894  addclpr  7897  nqprm  7902  mullocprlem  7930  mullocpr  7931  mulclpr  7932  ltpopr  7955  ltaddpr  7957  ltexprlemm  7960  ltexprlemopl  7961  ltexprlemopu  7963  ltexprlemrnd  7965  ltexprlemdisj  7966  addcanprleml  7974  addcanprlemu  7975  addcanprg  7976  recexprlemm  7984  recexprlemopl  7985  recexprlemopu  7987  recexprlemrnd  7989  recexprlemdisj  7990  cauappcvgprlemm  8005  cauappcvgprlemopl  8006  cauappcvgprlemopu  8008  cauappcvgprlemrnd  8010  cauappcvgprlemdisj  8011  cauappcvgprlemlim  8021  caucvgprlemnkj  8026  caucvgprlemm  8028  caucvgprlemopl  8029  caucvgprlemopu  8031  caucvgprlemrnd  8033  caucvgprlemlim  8041  caucvgprprlemnkltj  8049  caucvgprprlemnkeqj  8050  caucvgprprlemnjltk  8051  caucvgprprlemm  8056  caucvgprprlemopl  8057  caucvgprprlemopu  8059  caucvgprprlemrnd  8061  caucvgprprlemexbt  8066  caucvgprprlemlim  8071  suplocexprlemrl  8077  suplocexprlemru  8079  suplocexprlemdisj  8080  suplocexprlemloc  8081  suplocexprlemex  8082  suplocexprlemub  8083  prsrlem1  8102  mulclsr  8114  mulasssrg  8118  distrsrg  8119  suplocsrlemb  8166  elreal2  8190  axmulass  8233  axdistr  8234  axcaucvglemcau  8258  add20  8795  mullt0  8801  rereim  8907  ltmul1  8913  cru  8923  mulap0r  8936  aprcl  8967  aptap  8971  divmuldivap  9035  divmuleqap  9040  divadddivap  9050  divmuldivapd  9155  divmuleqapd  9156  div2subap  9160  ltmul12a  9183  lemul12a  9185  lemulge11  9189  lediv12a  9217  lediv2a  9218  recgt1i  9221  recreclt  9223  ledivp1  9226  lemul1ad  9262  lemul2ad  9263  ltmul12ad  9264  lemul12ad  9265  lemul12bd  9266  nndivre  9322  nndivtr  9328  halfaddsubcl  9520  halfaddsub  9521  lt2halves  9523  nnrecl  9543  elnn0nn  9587  elnnnn0b  9589  elnnnn0c  9590  nn0addge1  9591  nn0addge2  9592  xnn0xrnemnf  9624  elnn0z  9639  elnnz1  9649  nzadd  9679  elz2  9698  zdivadd  9717  zdivmul  9718  zextle  9719  peano2uz2  9735  uzind  9739  btwnz  9747  uzss  9925  eluzp1m1  9928  infregelbex  9980  eluz2b2  9985  qre  10007  qaddcl  10017  qmulcl  10019  qreccl  10024  irradd  10028  irrmul  10029  elpqb  10032  cnref1o  10033  rprege0  10051  rprene0  10054  rpreap0  10055  rpcnne0  10056  rpcnap0  10057  rpregt0d  10086  rprege0d  10087  rprene0d  10088  rpcnne0d  10089  lediv2ad  10102  ledivge1le  10109  lediv12ad  10139  nnledivrp  10149  nn0ledivnn  10150  xrlttri3  10181  xrrebnd  10203  xrrege0  10209  xnn0xadd0  10251  xlesubadd  10267  elioo4g  10318  ioomax  10332  iccmax  10333  divelunit  10386  elfz5  10402  uzsubsubfz  10433  fzopth  10448  fzass4  10449  fzrev2  10473  uzsplit  10480  elfz2nn0  10500  difelfzle  10522  1fv  10527  4fvwrd4  10528  fzo1fzo0n0  10576  elfzom1elp1fzo  10601  subfzo0  10642  infssuzex  10647  infssfzcldc  10650  infssfzledc  10651  qtri3or  10656  adddivflid  10708  flltdivnn0lt  10720  intfracq  10738  modqid2  10769  modfzo0difsn  10813  seq3val  10878  seqvalcd  10879  iseqf1olemqcl  10917  iseqf1olemnab  10919  iseqf1olemab  10920  iseqf1olemmo  10923  seq3f1olemqsumkj  10929  seq3f1olemqsumk  10930  seqf1oglem1  10937  seqf1oglem2  10938  expclzaplem  10981  leexp1a  11012  expubnd  11014  le2sq2  11033  sumsqeq0  11036  bernneq  11079  expnlbnd  11083  nn0opthd  11141  faclbnd6  11163  facavg  11165  sseqn  11260  hashfibclem  11263  hashf1lem2  11267  seq3coll  11275  hash2en  11276  wrdnval  11316  ccat0  11345  ccatsymb  11351  ccatalpha  11362  swrdspsleq  11420  pfxtrcfv  11446  pfxsuffeqwrdeq  11451  wrd2ind  11476  pfxccatin12lem2a  11480  pfxccatin12  11486  pfxccat3  11487  swrdccat  11488  pfxccatpfx1  11489  pfxccatpfx2  11490  swrdccatin1d  11496  swrdccatin2d  11497  shftlem  11562  shftfvalg  11564  shftfval  11567  cvg1nlemcau  11731  cvg1nlemres  11732  rexuz3  11737  resqrexlemcvg  11766  resqrexlemglsq  11769  resqrexlemga  11770  sqrtle  11783  sqrtlt  11784  sqrt11  11786  sqrtsq2  11790  absmul  11816  sqabs  11829  abslt  11835  absle  11836  lenegsq  11842  maxleastb  11961  maxltsup  11965  rexanre  11967  negfi  11975  xrmaxiflemab  11994  xrmaxiflemlub  11995  xrmaxltsup  12005  xrmaxadd  12008  climcn2  12056  mulcn2  12059  summodclem2a  12129  summodc  12131  fsum3  12135  fsum3cvg3  12144  fsumcl2lem  12146  fsumadd  12154  fsump1i  12181  fsum0diaglem  12188  mptfzshft  12190  fsumrev  12191  fsummulc2  12196  fsum00  12210  expcnvap0  12250  mertenslemi1  12283  ntrivcvgap0  12297  prodmodclem3  12323  prodmodclem2a  12324  zproddc  12327  fprodseq  12331  fprodrev  12367  fprodconst  12368  eftlub  12438  efieq  12483  sincos1sgn  12513  demoivreALT  12522  dvdsval3  12539  dvdscmul  12566  dvdsmulc  12567  dvdscmulr  12568  dvdsmulcr  12569  modmulconst  12571  dvds2ln  12572  ltoddhalfle  12641  nn0o  12655  divalg2  12674  ndvdssub  12678  ndvdsadd  12679  divgcdz  12729  gcd0id  12737  gcdaddm  12742  bezoutlemstep  12755  bezoutlemmain  12756  dfgcd3  12768  dfgcd2  12772  lcmcllem  12826  dvdslcm  12828  lcmgcdlem  12836  lcmgcdnn  12841  qredeq  12855  qredeu  12856  rpdvds  12858  divgcdcoprm0  12860  cncongr1  12862  cncongr2  12863  cncongrcoprm  12865  prmind2  12879  isprm5  12901  isprm6  12906  prmexpb  12910  cncongrprm  12916  sqrt2irrlem  12920  pw2dvdslemn  12924  oddpwdclemxy  12928  oddpwdclemdc  12932  oddpwdc  12933  hashdvds  12980  prmdiv  12994  hashgcdlem  12997  nnoddn2prmb  13022  pythagtriplem6  13030  pythagtriplem7  13031  pcpre1  13052  pccl  13059  pcmul  13061  pcdiv  13062  pcqmul  13063  pcqcl  13066  pcdvds  13075  pcndvds  13077  pcndvds2  13079  pc2dvds  13090  dvdsprmpweqle  13097  difsqpwdvds  13098  pcaddlem  13099  pcadd  13100  pcmptcl  13102  pcmpt  13103  fldivp1  13108  pcfac  13110  oddprmdvds  13114  infpnlem2  13120  4sqlem5  13142  4sqlem6  13143  4sqlem4a  13151  4sqexercise1  13158  4sqexercise2  13159  4sqlem13m  13163  4sqlem15  13165  4sqlem16  13166  ballotfilem2  13209  ballotfilemfp1  13212  ballotfilemsf1o  13238  ballotfilemrinv0  13257  ballotfilem7  13260  ballotfilemth  13262  ennnfonelemfun  13289  ennnfonelemim  13296  ctinfomlemom  13299  ctinfom  13300  ctinf  13302  ctiunctlemfo  13311  omctfn  13315  fnpr2ob  13641  ismgmid2  13680  fngzsum  13688  gzsumvalx  13689  gzsumfzval  13691  gzsum0  13693  gzsumval2  13694  issgrpd  13707  ismndd  13730  imasmnd2  13739  mhmf1o  13757  subsubm  13770  dfgrp2  13812  isgrpid2  13825  isgrpinv  13839  grplrinv  13842  dfgrp3mlem  13883  dfgrp3m  13884  dfgrp3me  13885  imasgrp2  13893  mhmmnd  13899  issubg2m  13972  issubgrpd2  13973  grpissubg  13977  subsubg  13980  subgintm  13981  isnsg3  13990  nmzsubg  13993  eqgval  14006  eqgen  14010  isghmd  14035  ghmrn  14040  ghmpreima  14049  ghmf1o  14058  conjghm  14059  conjnmzb  14063  ghmpropd  14066  rinvmod  14093  imasabl  14120  gsumvalfi  14132  gsump1  14137  prdsidlem  14173  prdsinvlem  14176  rnglz  14222  isrngd  14230  rng1zr  14237  srgdilem  14250  srg1zr  14268  srglmhm  14274  srgrmhm  14275  ringdilem  14293  isringd  14322  ringsrg  14328  ringinvnzdiv  14331  imasring  14345  dvdsrd  14377  unitgrp  14399  isrim0  14444  isrhm2d  14448  rhmf1o  14451  rhmco  14457  rhmopp  14459  issubrng2  14494  subsubrng  14498  subrgugrp  14524  issubrg2  14525  subsubrg  14529  resrhm  14532  ringunitap  14569  aprap  14574  drngunitap  14584  lmodfopnelem2  14637  lsssubg  14689  islss3  14691  islss4  14694  lspsnel6  14720  lidlacl  14796  lidlsubg  14798  lidlrsppropdg  14807  2idlelbas  14828  cnfld1  14884  cnsubglem  14891  mulgghm2  14918  zndvds  14959  psrbagcon  14988  mplsubgfi  15018  topgele  15056  tgcl  15091  epttop  15117  opnssneib  15183  iscnp4  15245  cnco  15248  cncnp  15257  cnrest2  15263  lmss  15273  txcnp  15298  txcn  15302  cnmpt12  15314  cnmpt22  15321  hmeof1o  15336  psmetres2  15360  distspace  15362  ismeti  15373  isxmetd  15374  xmetpsmet  15396  xblss2ps  15431  xblss2  15432  blcntrps  15442  blcntr  15443  blin2  15459  mopni3  15511  metequiv2  15523  bdmet  15529  xmettx  15537  cnbl0  15561  cnblcld  15562  tgioo  15581  elcncf1di  15606  dedekindeulemlu  15648  suplociccex  15652  dedekindicclemlu  15657  dedekindicc  15660  ivthinclemlopn  15663  ivthdec  15671  ivthreinc  15672  ivthdichlem  15678  cnplimcim  15694  limccnp2lem  15703  dvfvalap  15708  plymullem  15777  reeff1olem  15798  sin0pilem1  15808  pilem3  15810  ptolemy  15851  sincosq1sgn  15853  sinq12gt0  15857  ioocosf1o  15881  rprelogbmulexp  15984  pellexlem3  16010  perfectlem2  16031  lgslem3  16038  lgsne0  16074  gausslemma2dlem0b  16086  gausslemma2dlem0c  16087  lgsquadlem2  16114  lgsquad2lem2  16118  2lgsoddprmlem2  16142  2sqlem8  16159  gropd  16205  grstructd2dom  16206  incistruhgr  16248  umgrislfupgrenlem  16288  umgrislfupgrdom  16289  uspgrupgrushgr  16340  usgrumgruspgr  16343  usgruspgrben  16344  usgrislfuspgrdom  16348  umgrvad2edg  16369  umgr2edgneu  16370  ushgredgedg  16384  ushgredgedgloop  16386  subgrprop3  16420  iswlkg  16487  wlk2f  16509  upgriswlkdc  16518  wlkv0  16527  wlklenvclwlk  16531  wlkepvtx  16533  upgr2wlkdc  16535  wlkres  16537  clwwlkccatlem  16558  clwwlkccat  16559  clwwlknbp  16573  clwwlknp  16575  clwwlkext2edg  16580  clwwlknon  16587  clwwlknonccat  16591  clwwlknonex2  16597  clwwlknonex2e  16598  trlsegvdeglem1  16618  dichmul0orlem3  16672  bj-nnan  16681  bj-charfun  16750  bdop  16818  bdunexb  16863  bj-om  16880  findset  16888  bj-peano4  16898  bj-inf2vn  16917  bj-inf2vn2  16918  pwle2  16945  pwf1oexmid  16946  nnnninfex  16973  sbthom  16979  qdencn  16980  trilpolemlt1  16998