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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used 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  3773  prel12  3896  prneimg  3899  preqsn  3900  disjiun  4125  opth  4379  0nelop  4390  euotd  4397  opelopabsb  4404  ispod  4451  elon2  4523  unexb  4590  opeluu  4598  eusvnfb  4602  suc11g  4706  nlimsucg  4715  tfi  4731  vtoclr  4825  opthprc  4828  ideqg  4933  resiexg  5111  dminss  5205  imainss  5206  ssxpbm  5226  relrelss  5317  funopg  5414  fununfun  5427  fntpg  5440  fun11uni  5454  imain  5466  funimaexglem  5467  funssxp  5560  ffdm  5561  f00  5587  dffo2  5622  fodmrnu  5626  foco  5629  fun11iun  5663  f1o00  5679  fsnd  5687  fv3  5721  fvun1d  5774  fvun2d  5775  dff2  5855  dff3im  5856  dffo4  5859  ffnfv  5869  ffvresb  5874  fsn2  5885  fconstfvm  5936  fnfvima  5956  resfvresima  5959  fcof1o  5998  isocnv  6020  isotr  6025  riotaprop  6067  acexmidlemcase  6083  caovlem2d  6285  f1ocnvd  6295  f1o3d  6301  caofcom  6337  resfunexgALT  6341  elxp7  6408  2ndrn  6421  1stconst  6461  2ndconst  6462  cnvf1olem  6464  poxp  6472  ressuppss  6498  funsssuppss  6502  dftpos4  6539  dfsmo2  6563  tfrlem5  6590  tfrlemiex  6607  tfr1onlemsucaccv  6617  tfr1onlembfn  6620  tfr1onlemex  6623  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembfn  6633  tfrcllemex  6636  tfrcllemres  6638  tfrcl  6640  frecabex  6674  frecabcl  6675  frecfcllem  6680  frecrdg  6684  oawordi  6747  nntri3  6775  nntr2  6781  nnmordi  6794  iserd  6838  relelec  6854  erth  6858  qliftfun  6896  mapsnd  6976  mapsncnv  6983  mptelixpg  7022  bren  7036  pw2f1odclem  7140  mapunen  7157  findcard2d  7201  findcard2sd  7202  isinfinf  7207  tridc  7210  nnwetri  7229  undifdcss  7236  fiintim  7244  fisseneq  7248  fidcenumlemim  7276  sbthlemi9  7289  supisolem  7354  ordiso2  7381  updjud  7428  difinfsn  7446  ctssdccl  7457  nnnninfeq  7474  omniwomnimkv  7513  pr2cv  7549  acfun  7569  exmidontriimlem2  7584  onntri45  7606  dftap2  7623  netap  7626  2omotaplemap  7629  ccfunen  7636  cc4f  7641  cc4n  7643  elni2  7687  dfplpq2  7727  dfmpq2  7728  enqbreq2  7730  enqdc1  7735  addcmpblnq  7740  addclnq  7748  nqpi  7751  addassnqg  7755  mulassnqg  7757  mulcanenq  7758  distrnqg  7760  1qec  7761  recexnq  7763  subhalfnqq  7787  enq0tr  7807  nqnq0pi  7811  nq0nn  7815  mulcanenq0ec  7818  nnnq0lem1  7819  addclnq0  7824  distrnq0  7832  addassnq0lemcl  7834  elnp1st2nd  7849  prarloc  7876  addlocprlemlt  7904  addlocprlemeq  7906  addlocprlemgt  7907  addclpr  7910  nqprm  7915  mullocprlem  7943  mullocpr  7944  mulclpr  7945  ltpopr  7968  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemrnd  7978  ltexprlemdisj  7979  addcanprleml  7987  addcanprlemu  7988  addcanprg  7989  recexprlemm  7997  recexprlemopl  7998  recexprlemopu  8000  recexprlemrnd  8002  recexprlemdisj  8003  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemrnd  8023  cauappcvgprlemdisj  8024  cauappcvgprlemlim  8034  caucvgprlemnkj  8039  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemrnd  8046  caucvgprlemlim  8054  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemm  8069  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemrnd  8074  caucvgprprlemexbt  8079  caucvgprprlemlim  8084  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  prsrlem1  8115  mulclsr  8127  mulasssrg  8131  distrsrg  8132  suplocsrlemb  8179  elreal2  8203  axmulass  8246  axdistr  8247  axcaucvglemcau  8271  add20  8809  mullt0  8815  rereim  8922  ltmul1  8928  cru  8938  mulap0r  8951  aprcl  8982  aptap  8986  divmuldivap  9050  divmuleqap  9055  divadddivap  9065  divmuldivapd  9170  divmuleqapd  9171  div2subap  9175  ltmul12a  9198  lemul12a  9200  lemulge11  9204  lediv12a  9232  lediv2a  9233  recgt1i  9236  recreclt  9238  ledivp1  9241  lemul1ad  9277  lemul2ad  9278  ltmul12ad  9279  lemul12ad  9280  lemul12bd  9281  nndivre  9349  nndivtr  9355  halfaddsubcl  9549  halfaddsub  9550  lt2halves  9552  nnrecl  9572  elnn0nn  9616  elnnnn0b  9618  elnnnn0c  9619  nn0addge1  9620  nn0addge2  9621  xnn0xrnemnf  9651  elnn0z  9666  elnnz1  9676  nzadd  9706  elz2  9725  zdivadd  9745  zdivmul  9746  zextle  9747  peano2uz2  9763  uzind  9767  btwnz  9775  uzss  9958  eluzp1m1  9961  infregelbex  10013  eluz2b2  10018  qre  10040  qaddcl  10050  qmulcl  10052  qreccl  10057  irradd  10061  irraddap  10062  irrmul  10063  elpqb  10066  cnref1o  10067  rprege0  10085  rprene0  10088  rpreap0  10089  rpcnne0  10090  rpcnap0  10091  rpregt0d  10120  rprege0d  10121  rprene0d  10122  rpcnne0d  10123  lediv2ad  10136  ledivge1le  10143  lediv12ad  10173  nnledivrp  10183  nn0ledivnn  10184  xrlttri3  10215  xrrebnd  10237  xrrege0  10243  xnn0xadd0  10285  xlesubadd  10301  elioo4g  10352  ioomax  10366  iccmax  10367  divelunit  10420  elfz5  10436  uzsubsubfz  10468  fzopth  10483  fzass4  10484  fzrev2  10508  uzsplit  10515  elfz2nn0  10535  difelfzle  10557  1fv  10562  4fvwrd4  10563  fzo1fzo0n0  10611  elfzom1elp1fzo  10636  subfzo0  10677  infssuzex  10682  infssfzcldc  10685  infssfzledc  10686  qtri3or  10691  adddivflid  10747  flltdivnn0lt  10759  intfracq  10777  modqid2  10808  modfzo0difsn  10852  seq3val  10917  seqvalcd  10918  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemmo  10962  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seqf1oglem1  10976  seqf1oglem2  10977  expclzaplem  11020  leexp1a  11051  expubnd  11053  le2sq2  11072  sumsqeq0  11075  bernneq  11118  expnlbnd  11122  nn0sqdc  11167  nn0opthd  11181  faclbnd6  11203  facavg  11205  sseqn  11300  hashfibclem  11303  hashf1lem2  11307  seq3coll  11315  hash2en  11316  wrdnval  11356  ccat0  11385  ccatsymb  11391  ccatalpha  11402  swrdspsleq  11460  pfxtrcfv  11486  pfxsuffeqwrdeq  11491  wrd2ind  11516  pfxccatin12lem2a  11520  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  pfxccatpfx1  11529  pfxccatpfx2  11530  swrdccatin1d  11536  swrdccatin2d  11537  shftlem  11602  shftfvalg  11604  shftfval  11607  cvg1nlemcau  11771  cvg1nlemres  11772  rexuz3  11777  resqrexlemcvg  11806  resqrexlemglsq  11809  resqrexlemga  11810  sqrtle  11823  sqrtlt  11824  sqrt11  11826  sqrtsq2  11830  absmul  11856  sqabs  11870  abslt  11876  absle  11877  lenegsq  11883  maxleastb  12002  maxltsup  12006  rexanre  12008  negfi  12016  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxltsup  12048  xrmaxadd  12051  climcn2  12099  mulcn2  12102  summodclem2a  12172  summodc  12174  fsum3  12178  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  fsump1i  12224  fsum0diaglem  12231  mptfzshft  12233  fsumrev  12234  fsummulc2  12239  fsum00  12253  expcnvap0  12293  mertenslemi1  12326  ntrivcvgap0  12340  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodrev  12410  fprodconst  12411  eftlub  12481  efieq  12526  sincos1sgn  12556  demoivreALT  12565  dvdsval3  12582  dvdscmul  12609  dvdsmulc  12610  dvdscmulr  12611  dvdsmulcr  12612  modmulconst  12614  dvds2ln  12615  ltoddhalfle  12684  nn0o  12698  divalg2  12717  ndvdssub  12721  ndvdsadd  12722  divgcdz  12772  gcd0id  12780  gcdaddm  12785  bezoutlemstep  12798  bezoutlemmain  12799  dfgcd3  12811  dfgcd2  12815  lcmcllem  12869  dvdslcm  12871  lcmgcdlem  12879  lcmgcdnn  12884  qredeq  12898  qredeu  12899  rpdvds  12901  divgcdcoprm0  12903  cncongr1  12905  cncongr2  12906  cncongrcoprm  12908  prmind2  12922  isprm5  12945  isprm6  12950  prmexpb  12954  cncongrprm  12960  sqrt2irrlem  12964  pwbdvdslemn  12968  nnmaxpwlemxy  12972  nnmaxpwlemparts  12976  nnmaxpw  12977  hashdvds  13027  prmdiv  13041  hashgcdlem  13044  nnoddn2prmb  13069  pythagtriplem6  13077  pythagtriplem7  13078  pcpre1  13099  pccl  13106  pcmul  13108  pcdiv  13109  pcqmul  13110  pcqcl  13113  pcdvds  13122  pcndvds  13124  pcndvds2  13126  pc2dvds  13137  dvdsprmpweqle  13144  difsqpwdvds  13145  pcaddlem  13146  pcadd  13147  pcmptcl  13149  pcmpt  13150  fldivp1  13155  pcfac  13157  oddprmdvds  13161  infpnlem2  13167  4sqlem5  13189  4sqlem6  13190  4sqlem4a  13198  4sqexercise1  13205  4sqexercise2  13206  4sqlem13m  13210  4sqlem15  13212  4sqlem16  13213  ballotfilem2  13285  ballotfilemfp1  13288  ballotfilemsf1o  13314  ballotfilemrinv0  13333  ballotfilem7  13336  ballotfilemth  13338  ennnfonelemfun  13365  ennnfonelemim  13372  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  ctiunctlemfo  13387  omctfn  13391  fnpr2ob  13719  ismgmid2  13758  fngzsum  13766  gzsumvalx  13767  gzsumfzval  13769  gzsum0  13771  gzsumval2  13772  issgrpd  13785  ismndd  13808  imasmnd2  13817  mhmf1o  13835  subsubm  13848  dfgrp2  13890  isgrpid2  13903  isgrpinv  13917  grplrinv  13920  dfgrp3mlem  13961  dfgrp3m  13962  dfgrp3me  13963  imasgrp2  13971  mhmmnd  13977  issubg2m  14050  issubgrpd2  14051  grpissubg  14055  subsubg  14058  subgintm  14059  isnsg3  14068  nmzsubg  14071  eqgval  14084  eqgen  14088  isghmd  14113  ghmrn  14118  ghmpreima  14127  ghmf1o  14136  conjghm  14137  conjnmzb  14141  ghmpropd  14144  cntzrcl  14158  rinvmod  14202  imasabl  14229  gsumvalfi  14241  gsump1  14246  prdsidlem  14299  prdsinvlem  14302  rnglz  14350  isrngd  14358  rng1zr  14365  srgdilem  14379  srg1zr  14397  srglmhm  14403  srgrmhm  14404  ringdilem  14422  isringd  14452  ringsrg  14458  ringinvnzdiv  14461  imasring  14477  dvdsrd  14509  unitgrp  14531  isrim0  14576  isrhm2d  14580  rhmf1o  14583  rhmco  14589  rhmopp  14591  issubrng2  14626  subsubrng  14630  subrgugrp  14656  issubrg2  14657  subsubrg  14661  resrhm  14664  ringunitap  14701  aprap  14706  drngunitap  14716  lmodfopnelem2  14770  lsssubg  14822  islss3  14824  islss4  14827  ellspsn6  14853  lidlacl  14929  lidlsubg  14931  lidlrsppropdg  14940  2idlelbas  14961  cnfld1  15017  cnsubglem  15024  mulgghm2  15051  zndvds  15092  isassad  15119  issubassa  15121  assapropd  15122  psrbagcon  15174  gsumbagdiaglem  15184  mplsubgfi  15234  topgele  15272  tgcl  15307  epttop  15333  opnssneib  15399  iscnp4  15461  cnco  15464  cncnp  15473  cnrest2  15479  lmss  15489  txcnp  15514  txcn  15518  cnmpt12  15530  cnmpt22  15537  hmeof1o  15552  psmetres2  15576  distspace  15578  ismeti  15589  isxmetd  15590  xmetpsmet  15612  xblss2ps  15647  xblss2  15648  blcntrps  15658  blcntr  15659  blin2  15675  mopni3  15727  metequiv2  15739  bdmet  15745  xmettx  15753  cnbl0  15777  cnblcld  15778  tgioo  15797  elcncf1di  15822  dedekindeulemlu  15864  suplociccex  15868  dedekindicclemlu  15873  dedekindicc  15876  ivthinclemlopn  15879  ivthdec  15887  ivthreinc  15888  ivthdichlem  15894  cnplimcim  15910  limccnp2lem  15919  dvfvalap  15924  plymullem  15993  reeff1olem  16014  sin0pilem1  16025  pilem3  16027  ptolemy  16068  sincosq1sgn  16070  sinq12gt0  16074  ioocosf1o  16099  rprelogbmulexp  16209  zprmlogbaplem2  16233  pellexlem3  16248  chtublem  16312  perfectlem2  16317  bcmono  16321  bclbnd  16324  bposlem5  16332  bposlem6  16333  lgslem3  16343  lgsne0  16379  gausslemma2dlem0b  16391  gausslemma2dlem0c  16392  lgsquadlem2  16419  lgsquad2lem2  16423  2lgsoddprmlem2  16447  2sqlem8  16464  gropd  16510  grstructd2dom  16511  incistruhgr  16553  umgrislfupgrenlem  16593  umgrislfupgrdom  16594  uspgrupgrushgr  16645  usgrumgruspgr  16648  usgruspgrben  16649  usgrislfuspgrdom  16653  umgrvad2edg  16674  umgr2edgneu  16675  ushgredgedg  16689  ushgredgedgloop  16691  subgrprop3  16725  iswlkg  16792  wlk2f  16814  upgriswlkdc  16823  wlkv0  16832  wlklenvclwlk  16836  wlkepvtx  16838  upgr2wlkdc  16840  wlkres  16842  clwwlkccatlem  16863  clwwlkccat  16864  clwwlknbp  16878  clwwlknp  16880  clwwlkext2edg  16885  clwwlknon  16892  clwwlknonccat  16896  clwwlknonex2  16902  clwwlknonex2e  16903  trlsegvdeglem1  16923  dichmul0orlem3  16977  bj-nnan  16986  bj-charfun  17055  bdop  17123  bdunexb  17168  bj-om  17185  findset  17193  bj-peano4  17203  bj-inf2vn  17222  bj-inf2vn2  17223  pwle2  17250  pwf1oexmid  17251  nnnninfex  17288  sbthom  17294  qdencn  17295  trilpolemlt1  17314