Theorem jca 302

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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  jca31  305  jca32  306  jcai  307  jctil  308  jctir  309  ancli  319  ancri  320  sylanbrc  411  jcab  573  ioran  710  ordi  771  dfandc  822  stabtestimpdc  868  pm4.55dc  890  mpbi2and  895  mpbir2and  896  pm4.82  902  pm4.83dc  903  rnlem  928  syl22anc  1185  syl112anc  1188  syl121anc  1189  syl211anc  1190  syl23anc  1191  syl32anc  1192  syl122anc  1193  syl212anc  1194  syl221anc  1195  syl222anc  1200  syl123anc  1201  syl132anc  1202  syl213anc  1203  syl231anc  1204  syl312anc  1205  syl321anc  1206  syl223anc  1210  syl232anc  1211  syl322anc  1212  syl233anc  1213  syl323anc  1214  syl332anc  1215  ecased  1295  19.26  1425  nfand  1515  19.40  1578  equsexd  1675  sbcof2  1749  sbequ8  1786  eu2  2004  eu3h  2005  eu5  2007  mooran2  2033  datisi  2070  felapton  2074  darapti  2075  dimatis  2077  fresison  2078  fesapo  2080  reximssdv  2495  r19.26  2517  r19.29af2  2530  r19.40  2543  eqvinc  2762  eqvincg  2763  elrabd  2795  reu6  2826  reu3  2827  indifdir  3279  undif3ss  3284  un00  3356  eqifdc  3453  disjpr2  3534  prel12  3645  prneimg  3648  preqsn  3649  disjiun  3870  opth  4097  0nelop  4108  euotd  4114  opelopabsb  4120  ispod  4164  elon2  4236  unexb  4301  opeluu  4309  eusvnfb  4313  suc11g  4410  nlimsucg  4419  tfi  4434  vtoclr  4525  opthprc  4528  ideqg  4628  resiexg  4800  dminss  4889  imainss  4890  ssxpbm  4910  relrelss  5001  funopg  5093  fntpg  5115  fun11uni  5129  imain  5141  funimaexglem  5142  funssxp  5228  ffdm  5229  f00  5250  dffo2  5285  fodmrnu  5289  foco  5291  fun11iun  5322  f1o00  5336  fv3  5376  dff2  5496  dff3im  5497  dffo4  5500  ffnfv  5510  ffvresb  5515  fsn2  5526  fconstfvm  5570  fnfvima  5584  fcof1o  5622  isocnv  5644  isotr  5649  riotaprop  5685  acexmidlemcase  5701  caovlem2d  5895  f1ocnvd  5904  caofcom  5936  resfunexgALT  5939  elxp7  5999  2ndrn  6011  1stconst  6048  2ndconst  6049  cnvf1olem  6051  poxp  6059  dftpos4  6090  dfsmo2  6114  tfrlem5  6141  tfrlemiex  6158  tfr1onlemsucaccv  6168  tfr1onlembfn  6171  tfr1onlemex  6174  tfr1onlemres  6176  tfrcllemsucaccv  6181  tfrcllembfn  6184  tfrcllemex  6187  tfrcllemres  6189  tfrcl  6191  frecabex  6225  frecabcl  6226  frecfcllem  6231  frecrdg  6235  oawordi  6295  nntri3  6323  nntr2  6329  nnmordi  6342  iserd  6385  relelec  6399  erth  6403  qliftfun  6441  mapsncnv  6519  mptelixpg  6558  bren  6571  findcard2d  6714  findcard2sd  6715  isinfinf  6720  tridc  6722  nnwetri  6733  undifdcss  6740  fiintim  6746  fisseneq  6749  fidcenumlemim  6768  sbthlemi9  6781  supisolem  6810  ordiso2  6835  updjud  6882  difinfsn  6900  ctssdclemr  6911  elni2  7023  dfplpq2  7063  dfmpq2  7064  enqbreq2  7066  enqdc1  7071  addcmpblnq  7076  addclnq  7084  nqpi  7087  addassnqg  7091  mulassnqg  7093  mulcanenq  7094  distrnqg  7096  1qec  7097  recexnq  7099  subhalfnqq  7123  enq0tr  7143  nqnq0pi  7147  nq0nn  7151  mulcanenq0ec  7154  nnnq0lem1  7155  addclnq0  7160  distrnq0  7168  addassnq0lemcl  7170  elnp1st2nd  7185  prarloc  7212  addlocprlemlt  7240  addlocprlemeq  7242  addlocprlemgt  7243  addclpr  7246  nqprm  7251  mullocprlem  7279  mullocpr  7280  mulclpr  7281  ltpopr  7304  ltaddpr  7306  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemrnd  7314  ltexprlemdisj  7315  addcanprleml  7323  addcanprlemu  7324  addcanprg  7325  recexprlemm  7333  recexprlemopl  7334  recexprlemopu  7336  recexprlemrnd  7338  recexprlemdisj  7339  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemopu  7357  cauappcvgprlemrnd  7359  cauappcvgprlemdisj  7360  cauappcvgprlemlim  7370  caucvgprlemnkj  7375  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemopu  7380  caucvgprlemrnd  7382  caucvgprlemlim  7390  caucvgprprlemnkltj  7398  caucvgprprlemnkeqj  7399  caucvgprprlemnjltk  7400  caucvgprprlemm  7405  caucvgprprlemopl  7406  caucvgprprlemopu  7408  caucvgprprlemrnd  7410  caucvgprprlemexbt  7415  caucvgprprlemlim  7420  prsrlem1  7438  mulclsr  7450  mulasssrg  7454  distrsrg  7455  elreal2  7518  axmulass  7558  axdistr  7559  axcaucvglemcau  7583  add20  8103  mullt0  8109  rereim  8214  ltmul1  8220  cru  8230  mulap0r  8243  divmuldivap  8333  divmuleqap  8338  divadddivap  8348  divmuldivapd  8453  div2subap  8457  ltmul12a  8476  lemul12a  8478  lemulge11  8482  lediv12a  8510  lediv2a  8511  recgt1i  8514  recreclt  8516  ledivp1  8519  lemul1ad  8555  lemul2ad  8556  ltmul12ad  8557  lemul12ad  8558  lemul12bd  8559  nndivre  8614  nndivtr  8620  halfaddsubcl  8805  halfaddsub  8806  lt2halves  8807  nnrecl  8827  elnn0nn  8871  elnnnn0b  8873  elnnnn0c  8874  nn0addge1  8875  nn0addge2  8876  xnn0xrnemnf  8904  elnn0z  8919  elnnz1  8929  nzadd  8958  elz2  8974  zdivadd  8992  zdivmul  8993  zextle  8994  peano2uz2  9010  uzind  9014  btwnz  9022  uzss  9196  eluzp1m1  9199  eluz2b2  9247  qre  9267  qaddcl  9277  qmulcl  9279  qreccl  9284  irradd  9288  irrmul  9289  cnref1o  9290  rprege0  9305  rprene0  9308  rpreap0  9309  rpcnne0  9310  rpcnap0  9311  rpregt0d  9337  rprege0d  9338  rprene0d  9339  rpcnne0d  9340  lediv2ad  9353  ledivge1le  9360  lediv12ad  9390  nnledivrp  9394  nn0ledivnn  9395  xrlttri3  9424  xrrebnd  9443  xrrege0  9449  xnn0xadd0  9491  xlesubadd  9507  elioo4g  9558  ioomax  9572  iccmax  9573  divelunit  9626  elfz5  9639  uzsubsubfz  9668  fzopth  9682  fzass4  9683  fzrev2  9706  uzsplit  9713  elfz2nn0  9733  difelfzle  9752  1fv  9757  4fvwrd4  9758  fzo1fzo0n0  9801  elfzom1elp1fzo  9820  subfzo0  9860  qtri3or  9861  adddivflid  9906  flltdivnn0lt  9918  intfracq  9934  modqid2  9965  modfzo0difsn  10009  seq3val  10072  seqvalcd  10073  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemab  10103  iseqf1olemmo  10106  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  expclzaplem  10158  leexp1a  10189  expubnd  10191  le2sq2  10209  sumsqeq0  10212  bernneq  10253  expnlbnd  10257  nn0opthd  10309  faclbnd6  10331  facavg  10333  seq3coll  10426  shftlem  10429  shftfvalg  10431  shftfval  10434  cvg1nlemcau  10596  cvg1nlemres  10597  rexuz3  10602  resqrexlemcvg  10631  resqrexlemglsq  10634  resqrexlemga  10635  sqrtle  10648  sqrtlt  10649  sqrt11  10651  sqrtsq2  10655  absmul  10681  sqabs  10694  abslt  10700  absle  10701  lenegsq  10707  maxleastb  10826  maxltsup  10830  rexanre  10832  negfi  10838  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxltsup  10866  xrmaxadd  10869  climcn2  10917  mulcn2  10920  summodclem2a  10989  summodc  10991  fsum3  10995  fsum3cvg3  11004  fsumcl2lem  11006  fsumadd  11014  fsump1i  11041  fsum0diaglem  11048  mptfzshft  11050  fsumrev  11051  fsummulc2  11056  fsum00  11070  expcnvap0  11110  mertenslemi1  11143  eftlub  11194  efieq  11240  sincos1sgn  11269  demoivreALT  11277  dvdsval3  11292  dvdscmul  11315  dvdsmulc  11316  dvdscmulr  11317  dvdsmulcr  11318  modmulconst  11320  dvds2ln  11321  ltoddhalfle  11385  nn0o  11399  divalg2  11418  ndvdssub  11422  ndvdsadd  11423  infssuzex  11437  divgcdz  11455  gcd0id  11462  gcdaddm  11467  bezoutlemstep  11478  bezoutlemmain  11479  dfgcd3  11491  dfgcd2  11495  lcmcllem  11541  dvdslcm  11543  lcmgcdlem  11551  lcmgcdnn  11556  qredeq  11570  qredeu  11571  rpdvds  11573  divgcdcoprm0  11575  cncongr1  11577  cncongr2  11578  cncongrcoprm  11580  prmind2  11594  isprm6  11618  prmexpb  11622  cncongrprm  11628  sqrt2irrlem  11632  pw2dvdslemn  11635  oddpwdclemxy  11639  oddpwdclemdc  11643  oddpwdc  11644  hashdvds  11689  hashgcdlem  11695  ennnfonelemfun  11722  ennnfonelemim  11729  ctinfomlemom  11732  ctinfom  11733  ctinf  11735  topgele  11978  tgcl  12015  epttop  12041  opnssneib  12107  iscnp4  12168  cnco  12171  cncnp  12180  cnrest2  12186  lmss  12196  txcnp  12221  txcn  12225  cnmpt12  12237  cnmpt22  12244  psmetres2  12261  distspace  12263  ismeti  12274  isxmetd  12275  xmetpsmet  12297  xblss2ps  12332  xblss2  12333  blcntrps  12343  blcntr  12344  blin2  12360  mopni3  12412  metequiv2  12424  bdmet  12430  cnbl0  12456  cnblcld  12457  tgioo  12465  elcncf1di  12479  cnplimcim  12516  dvfvalap  12523  bdop  12654  bdunexb  12699  bj-om  12720  findset  12728  bj-peano4  12738  bj-inf2vn  12757  bj-inf2vn2  12758  pwle2  12779  pwf1oexmid  12780  nninfalllemn  12786  sbthom  12805  qdencn  12806  trilpolemlt1  12818