Theorem jca 300

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  jca31  302  jca32  303  jcai  304  jctil  305  jctir  306  ancli  316  ancri  317  sylanbrc  408  jcab  568  ioran  702  ordi  763  dfandc  812  stabtestimpdc  858  pm4.55dc  880  mpbi2and  885  mpbir2and  886  pm4.82  892  pm4.83dc  893  rnlem  918  syl22anc  1171  syl112anc  1174  syl121anc  1175  syl211anc  1176  syl23anc  1177  syl32anc  1178  syl122anc  1179  syl212anc  1180  syl221anc  1181  syl222anc  1186  syl123anc  1187  syl132anc  1188  syl213anc  1189  syl231anc  1190  syl312anc  1191  syl321anc  1192  syl223anc  1196  syl232anc  1197  syl322anc  1198  syl233anc  1199  syl323anc  1200  syl332anc  1201  ecased  1281  19.26  1411  nfand  1501  19.40  1563  equsexd  1659  sbcof2  1733  sbequ8  1770  eu2  1987  eu3h  1988  eu5  1990  mooran2  2016  datisi  2053  felapton  2057  darapti  2058  dimatis  2060  fresison  2061  fesapo  2063  r19.26  2491  r19.29af2  2502  r19.40  2514  eqvinc  2728  eqvincg  2729  elrabd  2761  reu6  2792  reu3  2793  indifdir  3238  undif3ss  3243  un00  3311  eqifdc  3404  disjpr2  3480  prel12  3589  prneimg  3592  preqsn  3593  opth  4028  0nelop  4039  euotd  4045  opelopabsb  4051  ispod  4095  elon2  4167  unexb  4231  opeluu  4236  eusvnfb  4240  suc11g  4336  nlimsucg  4345  tfi  4360  vtoclr  4444  opthprc  4447  ideqg  4545  resiexg  4714  dminss  4800  imainss  4801  ssxpbm  4820  relrelss  4911  funopg  5001  fntpg  5023  fun11uni  5037  imain  5049  funimaexglem  5050  funssxp  5129  ffdm  5130  f00  5150  dffo2  5185  fodmrnu  5189  foco  5191  fun11iun  5222  f1o00  5236  fv3  5273  dff2  5388  dff3im  5389  dffo4  5392  ffnfv  5398  ffvresb  5403  fsn2  5413  fconstfvm  5455  fnfvima  5469  fcof1o  5508  isocnv  5530  isotr  5535  riotaprop  5570  acexmidlemcase  5586  caovlem2d  5772  f1ocnvd  5781  caofcom  5813  resfunexgALT  5816  elxp7  5876  2ndrn  5888  1stconst  5921  2ndconst  5922  cnvf1olem  5924  poxp  5932  dftpos4  5960  dfsmo2  5984  tfrlem5  6011  tfrlemiex  6028  tfr1onlemsucaccv  6038  tfr1onlembfn  6041  tfr1onlemex  6044  tfr1onlemres  6046  tfrcllemsucaccv  6051  tfrcllembfn  6054  tfrcllemex  6057  tfrcllemres  6059  tfrcl  6061  frecabex  6095  frecabcl  6096  frecfcllem  6101  frecrdg  6105  oawordi  6162  nntri3  6190  nnmordi  6205  iserd  6248  relelec  6262  erth  6266  qliftfun  6304  mapsncnv  6382  bren  6394  findcard2d  6537  findcard2sd  6538  isinfinf  6543  nnwetri  6553  undifdcss  6560  fisseneq  6567  supisolem  6610  ordiso2  6635  updjud  6680  elni2  6776  dfplpq2  6816  dfmpq2  6817  enqbreq2  6819  enqdc1  6824  addcmpblnq  6829  addclnq  6837  nqpi  6840  addassnqg  6844  mulassnqg  6846  mulcanenq  6847  distrnqg  6849  1qec  6850  recexnq  6852  subhalfnqq  6876  enq0tr  6896  nqnq0pi  6900  nq0nn  6904  mulcanenq0ec  6907  nnnq0lem1  6908  addclnq0  6913  distrnq0  6921  addassnq0lemcl  6923  elnp1st2nd  6938  prarloc  6965  addlocprlemlt  6993  addlocprlemeq  6995  addlocprlemgt  6996  addclpr  6999  nqprm  7004  mullocprlem  7032  mullocpr  7033  mulclpr  7034  ltpopr  7057  ltaddpr  7059  ltexprlemm  7062  ltexprlemopl  7063  ltexprlemopu  7065  ltexprlemrnd  7067  ltexprlemdisj  7068  addcanprleml  7076  addcanprlemu  7077  addcanprg  7078  recexprlemm  7086  recexprlemopl  7087  recexprlemopu  7089  recexprlemrnd  7091  recexprlemdisj  7092  cauappcvgprlemm  7107  cauappcvgprlemopl  7108  cauappcvgprlemopu  7110  cauappcvgprlemrnd  7112  cauappcvgprlemdisj  7113  cauappcvgprlemlim  7123  caucvgprlemnkj  7128  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemopu  7133  caucvgprlemrnd  7135  caucvgprlemlim  7143  caucvgprprlemnkltj  7151  caucvgprprlemnkeqj  7152  caucvgprprlemnjltk  7153  caucvgprprlemm  7158  caucvgprprlemopl  7159  caucvgprprlemopu  7161  caucvgprprlemrnd  7163  caucvgprprlemexbt  7168  caucvgprprlemlim  7173  prsrlem1  7191  mulclsr  7203  mulasssrg  7207  distrsrg  7208  elreal2  7271  axmulass  7311  axdistr  7312  axcaucvglemcau  7336  add20  7855  mullt0  7861  rereim  7963  ltmul1  7969  cru  7979  mulap0r  7992  divmuldivap  8077  divmuleqap  8082  divadddivap  8092  divmuldivapd  8195  ltmul12a  8215  lemul12a  8217  lemulge11  8221  lediv12a  8249  lediv2a  8250  recgt1i  8253  recreclt  8255  ledivp1  8258  lemul1ad  8294  lemul2ad  8295  ltmul12ad  8296  lemul12ad  8297  lemul12bd  8298  nndivre  8351  nndivtr  8357  halfaddsubcl  8541  halfaddsub  8542  lt2halves  8543  nnrecl  8563  elnn0nn  8607  elnnnn0b  8609  elnnnn0c  8610  nn0addge1  8611  nn0addge2  8612  xnn0xrnemnf  8642  elnn0z  8659  elnnz1  8669  nzadd  8698  elz2  8714  zdivadd  8731  zdivmul  8732  zextle  8733  peano2uz2  8749  uzind  8753  btwnz  8761  uzss  8934  eluzp1m1  8937  eluz2b2  8985  qre  9005  qaddcl  9015  qmulcl  9017  qreccl  9022  irradd  9026  irrmul  9027  cnref1o  9028  rprege0  9043  rprene0  9046  rpreap0  9047  rpcnne0  9048  rpcnap0  9049  rpregt0d  9075  rprege0d  9076  rprene0d  9077  rpcnne0d  9078  lediv2ad  9091  ledivge1le  9098  lediv12ad  9128  nnledivrp  9132  nn0ledivnn  9133  xrlttri3  9162  xrrebnd  9176  xrrege0  9182  elioo4g  9247  ioomax  9261  iccmax  9262  divelunit  9314  elfz5  9327  uzsubsubfz  9356  fzopth  9369  fzass4  9370  fzrev2  9392  uzsplit  9399  elfz2nn0  9419  difelfzle  9436  1fv  9440  4fvwrd4  9441  fzo1fzo0n0  9483  elfzom1elp1fzo  9502  subfzo0  9542  qtri3or  9543  adddivflid  9588  flltdivnn0lt  9600  intfracq  9616  modqid2  9647  modfzo0difsn  9691  iseqvalt  9751  expclzaplem  9816  leexp1a  9847  expubnd  9849  le2sq2  9867  sumsqeq0  9870  bernneq  9909  expnlbnd  9913  nn0opthd  9965  faclbnd6  9987  facavg  9989  shftlem  10078  shftfvalg  10080  shftfval  10083  cvg1nlemcau  10244  cvg1nlemres  10245  rexuz3  10250  resqrexlemcvg  10279  resqrexlemglsq  10282  resqrexlemga  10283  sqrtle  10296  sqrtlt  10297  sqrt11  10299  sqrtsq2  10303  absmul  10329  sqabs  10342  abslt  10348  absle  10349  lenegsq  10355  maxleastb  10474  maxltsup  10478  rexanre  10480  negfi  10484  climcn2  10522  mulcn2  10525  dvdsval3  10580  dvdscmul  10603  dvdsmulc  10604  dvdscmulr  10605  dvdsmulcr  10606  modmulconst  10608  dvds2ln  10609  ltoddhalfle  10673  nn0o  10687  divalg2  10706  ndvdssub  10710  ndvdsadd  10711  infssuzex  10725  divgcdz  10743  gcd0id  10750  gcdaddm  10755  bezoutlemstep  10766  bezoutlemmain  10767  dfgcd3  10779  dfgcd2  10783  lcmcllem  10829  dvdslcm  10831  lcmgcdlem  10839  lcmgcdnn  10844  qredeq  10858  qredeu  10859  rpdvds  10861  divgcdcoprm0  10863  cncongr1  10865  cncongr2  10866  cncongrcoprm  10868  prmind2  10882  isprm6  10906  prmexpb  10910  cncongrprm  10916  sqrt2irrlem  10920  pw2dvdslemn  10923  oddpwdclemxy  10927  oddpwdclemdc  10931  oddpwdc  10932  hashdvds  10977  hashgcdlem  10983  bdop  11109  bdunexb  11154  bj-om  11175  findset  11183  bj-peano4  11193  bj-inf2vn  11212  bj-inf2vn2  11213  nninfalllemn  11239  qdencn  11253