Theorem jca 304

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 138	. 2 |- ( ps -> ( ch -> ( ps /\ ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jca31  307  jca32  308  jcai  309  jctil  310  jctir  311  ancli  321  ancri  322  sylanbrc  414  jcab  593  ioran  742  ordi  806  stdcndc  835  stdcndcOLD  836  dfandc  874  pm4.55dc  928  mpbi2and  933  mpbir2and  934  pm4.82  940  pm4.83dc  941  rnlem  966  syl22anc  1229  syl112anc  1232  syl121anc  1233  syl211anc  1234  syl23anc  1235  syl32anc  1236  syl122anc  1237  syl212anc  1238  syl221anc  1239  syl222anc  1244  syl123anc  1245  syl132anc  1246  syl213anc  1247  syl231anc  1248  syl312anc  1249  syl321anc  1250  syl223anc  1254  syl232anc  1255  syl322anc  1256  syl233anc  1257  syl323anc  1258  syl332anc  1259  ecased  1339  19.26  1469  nfand  1556  19.40  1619  equsexd  1717  sbcof2  1798  sbequ8  1835  eu2  2058  eu3h  2059  eu5  2061  mooran2  2087  datisi  2124  felapton  2128  darapti  2129  dimatis  2131  fresison  2132  fesapo  2134  reximssdv  2570  r19.26  2592  r19.29af2  2606  r19.40  2620  eqvinc  2849  eqvincg  2850  elrabd  2884  reu6  2915  reu3  2916  indifdir  3378  undif3ss  3383  un00  3455  eqifdc  3554  disjpr2  3640  prel12  3751  prneimg  3754  preqsn  3755  disjiun  3977  opth  4215  0nelop  4226  euotd  4232  opelopabsb  4238  ispod  4282  elon2  4354  unexb  4420  opeluu  4428  eusvnfb  4432  suc11g  4534  nlimsucg  4543  tfi  4559  vtoclr  4652  opthprc  4655  ideqg  4755  resiexg  4929  dminss  5018  imainss  5019  ssxpbm  5039  relrelss  5130  funopg  5222  fntpg  5244  fun11uni  5258  imain  5270  funimaexglem  5271  funssxp  5357  ffdm  5358  f00  5379  dffo2  5414  fodmrnu  5418  foco  5420  fun11iun  5453  f1o00  5467  fsnd  5475  fv3  5509  dff2  5629  dff3im  5630  dffo4  5633  ffnfv  5643  ffvresb  5648  fsn2  5659  fconstfvm  5703  fnfvima  5719  fcof1o  5757  isocnv  5779  isotr  5784  riotaprop  5821  acexmidlemcase  5837  caovlem2d  6034  f1ocnvd  6040  caofcom  6073  resfunexgALT  6076  elxp7  6138  2ndrn  6151  1stconst  6189  2ndconst  6190  cnvf1olem  6192  poxp  6200  dftpos4  6231  dfsmo2  6255  tfrlem5  6282  tfrlemiex  6299  tfr1onlemsucaccv  6309  tfr1onlembfn  6312  tfr1onlemex  6315  tfr1onlemres  6317  tfrcllemsucaccv  6322  tfrcllembfn  6325  tfrcllemex  6328  tfrcllemres  6330  tfrcl  6332  frecabex  6366  frecabcl  6367  frecfcllem  6372  frecrdg  6376  oawordi  6437  nntri3  6465  nntr2  6471  nnmordi  6484  iserd  6527  relelec  6541  erth  6545  qliftfun  6583  mapsncnv  6661  mptelixpg  6700  bren  6713  findcard2d  6857  findcard2sd  6858  isinfinf  6863  tridc  6865  nnwetri  6881  undifdcss  6888  fiintim  6894  fisseneq  6897  fidcenumlemim  6917  sbthlemi9  6930  supisolem  6973  ordiso2  7000  updjud  7047  difinfsn  7065  ctssdccl  7076  nnnninfeq  7092  omniwomnimkv  7131  acfun  7163  exmidontriimlem2  7178  onntri45  7197  ccfunen  7205  cc4f  7210  cc4n  7212  elni2  7255  dfplpq2  7295  dfmpq2  7296  enqbreq2  7298  enqdc1  7303  addcmpblnq  7308  addclnq  7316  nqpi  7319  addassnqg  7323  mulassnqg  7325  mulcanenq  7326  distrnqg  7328  1qec  7329  recexnq  7331  subhalfnqq  7355  enq0tr  7375  nqnq0pi  7379  nq0nn  7383  mulcanenq0ec  7386  nnnq0lem1  7387  addclnq0  7392  distrnq0  7400  addassnq0lemcl  7402  elnp1st2nd  7417  prarloc  7444  addlocprlemlt  7472  addlocprlemeq  7474  addlocprlemgt  7475  addclpr  7478  nqprm  7483  mullocprlem  7511  mullocpr  7512  mulclpr  7513  ltpopr  7536  ltaddpr  7538  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemrnd  7546  ltexprlemdisj  7547  addcanprleml  7555  addcanprlemu  7556  addcanprg  7557  recexprlemm  7565  recexprlemopl  7566  recexprlemopu  7568  recexprlemrnd  7570  recexprlemdisj  7571  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemopu  7589  cauappcvgprlemrnd  7591  cauappcvgprlemdisj  7592  cauappcvgprlemlim  7602  caucvgprlemnkj  7607  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemopu  7612  caucvgprlemrnd  7614  caucvgprlemlim  7622  caucvgprprlemnkltj  7630  caucvgprprlemnkeqj  7631  caucvgprprlemnjltk  7632  caucvgprprlemm  7637  caucvgprprlemopl  7638  caucvgprprlemopu  7640  caucvgprprlemrnd  7642  caucvgprprlemexbt  7647  caucvgprprlemlim  7652  suplocexprlemrl  7658  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemex  7663  suplocexprlemub  7664  prsrlem1  7683  mulclsr  7695  mulasssrg  7699  distrsrg  7700  suplocsrlemb  7747  elreal2  7771  axmulass  7814  axdistr  7815  axcaucvglemcau  7839  add20  8372  mullt0  8378  rereim  8484  ltmul1  8490  cru  8500  mulap0r  8513  aprcl  8544  divmuldivap  8608  divmuleqap  8613  divadddivap  8623  divmuldivapd  8728  divmuleqapd  8729  div2subap  8733  ltmul12a  8755  lemul12a  8757  lemulge11  8761  lediv12a  8789  lediv2a  8790  recgt1i  8793  recreclt  8795  ledivp1  8798  lemul1ad  8834  lemul2ad  8835  ltmul12ad  8836  lemul12ad  8837  lemul12bd  8838  nndivre  8893  nndivtr  8899  halfaddsubcl  9090  halfaddsub  9091  lt2halves  9092  nnrecl  9112  elnn0nn  9156  elnnnn0b  9158  elnnnn0c  9159  nn0addge1  9160  nn0addge2  9161  xnn0xrnemnf  9189  elnn0z  9204  elnnz1  9214  nzadd  9243  elz2  9262  zdivadd  9280  zdivmul  9281  zextle  9282  peano2uz2  9298  uzind  9302  btwnz  9310  uzss  9486  eluzp1m1  9489  infregelbex  9536  eluz2b2  9541  qre  9563  qaddcl  9573  qmulcl  9575  qreccl  9580  irradd  9584  irrmul  9585  elpqb  9587  cnref1o  9588  rprege0  9604  rprene0  9607  rpreap0  9608  rpcnne0  9609  rpcnap0  9610  rpregt0d  9639  rprege0d  9640  rprene0d  9641  rpcnne0d  9642  lediv2ad  9655  ledivge1le  9662  lediv12ad  9692  nnledivrp  9702  nn0ledivnn  9703  xrlttri3  9733  xrrebnd  9755  xrrege0  9761  xnn0xadd0  9803  xlesubadd  9819  elioo4g  9870  ioomax  9884  iccmax  9885  divelunit  9938  elfz5  9952  uzsubsubfz  9982  fzopth  9996  fzass4  9997  fzrev2  10020  uzsplit  10027  elfz2nn0  10047  difelfzle  10069  1fv  10074  4fvwrd4  10075  fzo1fzo0n0  10118  elfzom1elp1fzo  10137  subfzo0  10177  qtri3or  10178  adddivflid  10227  flltdivnn0lt  10239  intfracq  10255  modqid2  10286  modfzo0difsn  10330  seq3val  10393  seqvalcd  10394  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemab  10424  iseqf1olemmo  10427  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  expclzaplem  10479  leexp1a  10510  expubnd  10512  le2sq2  10530  sumsqeq0  10533  bernneq  10575  expnlbnd  10579  nn0opthd  10635  faclbnd6  10657  facavg  10659  seq3coll  10755  shftlem  10758  shftfvalg  10760  shftfval  10763  cvg1nlemcau  10926  cvg1nlemres  10927  rexuz3  10932  resqrexlemcvg  10961  resqrexlemglsq  10964  resqrexlemga  10965  sqrtle  10978  sqrtlt  10979  sqrt11  10981  sqrtsq2  10985  absmul  11011  sqabs  11024  abslt  11030  absle  11031  lenegsq  11037  maxleastb  11156  maxltsup  11160  rexanre  11162  negfi  11169  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxltsup  11199  xrmaxadd  11202  climcn2  11250  mulcn2  11253  summodclem2a  11322  summodc  11324  fsum3  11328  fsum3cvg3  11337  fsumcl2lem  11339  fsumadd  11347  fsump1i  11374  fsum0diaglem  11381  mptfzshft  11383  fsumrev  11384  fsummulc2  11389  fsum00  11403  expcnvap0  11443  mertenslemi1  11476  ntrivcvgap0  11490  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodrev  11560  fprodconst  11561  eftlub  11631  efieq  11676  sincos1sgn  11705  demoivreALT  11714  dvdsval3  11731  dvdscmul  11758  dvdsmulc  11759  dvdscmulr  11760  dvdsmulcr  11761  modmulconst  11763  dvds2ln  11764  ltoddhalfle  11830  nn0o  11844  divalg2  11863  ndvdssub  11867  ndvdsadd  11868  infssuzex  11882  divgcdz  11904  gcd0id  11912  gcdaddm  11917  bezoutlemstep  11930  bezoutlemmain  11931  dfgcd3  11943  dfgcd2  11947  lcmcllem  11999  dvdslcm  12001  lcmgcdlem  12009  lcmgcdnn  12014  qredeq  12028  qredeu  12029  rpdvds  12031  divgcdcoprm0  12033  cncongr1  12035  cncongr2  12036  cncongrcoprm  12038  prmind2  12052  isprm5  12074  isprm6  12079  prmexpb  12083  cncongrprm  12089  sqrt2irrlem  12093  pw2dvdslemn  12097  oddpwdclemxy  12101  oddpwdclemdc  12105  oddpwdc  12106  hashdvds  12153  prmdiv  12167  hashgcdlem  12170  nnoddn2prmb  12194  pythagtriplem6  12202  pythagtriplem7  12203  pcpre1  12224  pccl  12231  pcmul  12233  pcdiv  12234  pcqmul  12235  pcqcl  12238  pcdvds  12246  pcndvds  12248  pcndvds2  12250  pc2dvds  12261  dvdsprmpweqle  12268  difsqpwdvds  12269  pcaddlem  12270  pcadd  12271  pcmptcl  12272  pcmpt  12273  fldivp1  12278  pcfac  12280  oddprmdvds  12284  infpnlem2  12290  4sqlem5  12312  4sqlem6  12313  4sqlem4a  12321  ennnfonelemfun  12350  ennnfonelemim  12357  ctinfomlemom  12360  ctinfom  12361  ctinf  12363  ctiunctlemfo  12372  omctfn  12376  ismgmid2  12611  topgele  12667  tgcl  12704  epttop  12730  opnssneib  12796  iscnp4  12858  cnco  12861  cncnp  12870  cnrest2  12876  lmss  12886  txcnp  12911  txcn  12915  cnmpt12  12927  cnmpt22  12934  hmeof1o  12949  psmetres2  12973  distspace  12975  ismeti  12986  isxmetd  12987  xmetpsmet  13009  xblss2ps  13044  xblss2  13045  blcntrps  13055  blcntr  13056  blin2  13072  mopni3  13124  metequiv2  13136  bdmet  13142  xmettx  13150  cnbl0  13174  cnblcld  13175  tgioo  13186  elcncf1di  13206  dedekindeulemlu  13239  suplociccex  13243  dedekindicclemlu  13248  dedekindicc  13251  ivthinclemlopn  13254  ivthdec  13262  cnplimcim  13276  limccnp2lem  13285  dvfvalap  13290  reeff1olem  13332  sin0pilem1  13342  pilem3  13344  ptolemy  13385  sincosq1sgn  13387  sinq12gt0  13391  ioocosf1o  13415  rprelogbmulexp  13514  lgslem3  13543  lgsne0  13579  2sqlem8  13599  bj-nnan  13617  bj-charfun  13689  bdop  13757  bdunexb  13802  bj-om  13819  findset  13827  bj-peano4  13837  bj-inf2vn  13856  bj-inf2vn2  13857  pwle2  13878  pwf1oexmid  13879  sbthom  13905  qdencn  13906  trilpolemlt1  13920