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  814  stabtestimpdc  860  pm4.55dc  882  mpbi2and  887  mpbir2and  888  pm4.82  894  pm4.83dc  895  rnlem  920  syl22anc  1173  syl112anc  1176  syl121anc  1177  syl211anc  1178  syl23anc  1179  syl32anc  1180  syl122anc  1181  syl212anc  1182  syl221anc  1183  syl222anc  1188  syl123anc  1189  syl132anc  1190  syl213anc  1191  syl231anc  1192  syl312anc  1193  syl321anc  1194  syl223anc  1198  syl232anc  1199  syl322anc  1200  syl233anc  1201  syl323anc  1202  syl332anc  1203  ecased  1283  19.26  1413  nfand  1503  19.40  1565  equsexd  1661  sbcof2  1735  sbequ8  1772  eu2  1989  eu3h  1990  eu5  1992  mooran2  2018  datisi  2055  felapton  2059  darapti  2060  dimatis  2062  fresison  2063  fesapo  2065  r19.26  2493  r19.29af2  2504  r19.40  2517  eqvinc  2731  eqvincg  2732  elrabd  2764  reu6  2795  reu3  2796  indifdir  3244  undif3ss  3249  un00  3317  eqifdc  3411  disjpr2  3491  prel12  3600  prneimg  3603  preqsn  3604  opth  4040  0nelop  4051  euotd  4057  opelopabsb  4063  ispod  4107  elon2  4179  unexb  4243  opeluu  4248  eusvnfb  4252  suc11g  4348  nlimsucg  4357  tfi  4372  vtoclr  4456  opthprc  4459  ideqg  4557  resiexg  4726  dminss  4814  imainss  4815  ssxpbm  4834  relrelss  4925  funopg  5015  fntpg  5037  fun11uni  5051  imain  5063  funimaexglem  5064  funssxp  5146  ffdm  5147  f00  5167  dffo2  5202  fodmrnu  5206  foco  5208  fun11iun  5239  f1o00  5253  fv3  5293  dff2  5408  dff3im  5409  dffo4  5412  ffnfv  5421  ffvresb  5426  fsn2  5436  fconstfvm  5478  fnfvima  5492  fcof1o  5531  isocnv  5553  isotr  5558  riotaprop  5594  acexmidlemcase  5610  caovlem2d  5796  f1ocnvd  5805  caofcom  5837  resfunexgALT  5840  elxp7  5900  2ndrn  5912  1stconst  5945  2ndconst  5946  cnvf1olem  5948  poxp  5956  dftpos4  5984  dfsmo2  6008  tfrlem5  6035  tfrlemiex  6052  tfr1onlemsucaccv  6062  tfr1onlembfn  6065  tfr1onlemex  6068  tfr1onlemres  6070  tfrcllemsucaccv  6075  tfrcllembfn  6078  tfrcllemex  6081  tfrcllemres  6083  tfrcl  6085  frecabex  6119  frecabcl  6120  frecfcllem  6125  frecrdg  6129  oawordi  6186  nntri3  6214  nnmordi  6229  iserd  6272  relelec  6286  erth  6290  qliftfun  6328  mapsncnv  6406  bren  6418  findcard2d  6561  findcard2sd  6562  isinfinf  6567  tridc  6569  nnwetri  6580  undifdcss  6587  fisseneq  6595  sbthlemi9  6621  supisolem  6650  ordiso2  6675  updjud  6720  elni2  6820  dfplpq2  6860  dfmpq2  6861  enqbreq2  6863  enqdc1  6868  addcmpblnq  6873  addclnq  6881  nqpi  6884  addassnqg  6888  mulassnqg  6890  mulcanenq  6891  distrnqg  6893  1qec  6894  recexnq  6896  subhalfnqq  6920  enq0tr  6940  nqnq0pi  6944  nq0nn  6948  mulcanenq0ec  6951  nnnq0lem1  6952  addclnq0  6957  distrnq0  6965  addassnq0lemcl  6967  elnp1st2nd  6982  prarloc  7009  addlocprlemlt  7037  addlocprlemeq  7039  addlocprlemgt  7040  addclpr  7043  nqprm  7048  mullocprlem  7076  mullocpr  7077  mulclpr  7078  ltpopr  7101  ltaddpr  7103  ltexprlemm  7106  ltexprlemopl  7107  ltexprlemopu  7109  ltexprlemrnd  7111  ltexprlemdisj  7112  addcanprleml  7120  addcanprlemu  7121  addcanprg  7122  recexprlemm  7130  recexprlemopl  7131  recexprlemopu  7133  recexprlemrnd  7135  recexprlemdisj  7136  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemopu  7154  cauappcvgprlemrnd  7156  cauappcvgprlemdisj  7157  cauappcvgprlemlim  7167  caucvgprlemnkj  7172  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemopu  7177  caucvgprlemrnd  7179  caucvgprlemlim  7187  caucvgprprlemnkltj  7195  caucvgprprlemnkeqj  7196  caucvgprprlemnjltk  7197  caucvgprprlemm  7202  caucvgprprlemopl  7203  caucvgprprlemopu  7205  caucvgprprlemrnd  7207  caucvgprprlemexbt  7212  caucvgprprlemlim  7217  prsrlem1  7235  mulclsr  7247  mulasssrg  7251  distrsrg  7252  elreal2  7315  axmulass  7355  axdistr  7356  axcaucvglemcau  7380  add20  7899  mullt0  7905  rereim  8007  ltmul1  8013  cru  8023  mulap0r  8036  divmuldivap  8121  divmuleqap  8126  divadddivap  8136  divmuldivapd  8239  ltmul12a  8259  lemul12a  8261  lemulge11  8265  lediv12a  8293  lediv2a  8294  recgt1i  8297  recreclt  8299  ledivp1  8302  lemul1ad  8338  lemul2ad  8339  ltmul12ad  8340  lemul12ad  8341  lemul12bd  8342  nndivre  8395  nndivtr  8401  halfaddsubcl  8585  halfaddsub  8586  lt2halves  8587  nnrecl  8607  elnn0nn  8651  elnnnn0b  8653  elnnnn0c  8654  nn0addge1  8655  nn0addge2  8656  xnn0xrnemnf  8684  elnn0z  8699  elnnz1  8709  nzadd  8738  elz2  8754  zdivadd  8771  zdivmul  8772  zextle  8773  peano2uz2  8789  uzind  8793  btwnz  8801  uzss  8974  eluzp1m1  8977  eluz2b2  9025  qre  9045  qaddcl  9055  qmulcl  9057  qreccl  9062  irradd  9066  irrmul  9067  cnref1o  9068  rprege0  9083  rprene0  9086  rpreap0  9087  rpcnne0  9088  rpcnap0  9089  rpregt0d  9115  rprege0d  9116  rprene0d  9117  rpcnne0d  9118  lediv2ad  9131  ledivge1le  9138  lediv12ad  9168  nnledivrp  9172  nn0ledivnn  9173  xrlttri3  9202  xrrebnd  9216  xrrege0  9222  elioo4g  9287  ioomax  9301  iccmax  9302  divelunit  9354  elfz5  9367  uzsubsubfz  9396  fzopth  9409  fzass4  9410  fzrev2  9432  uzsplit  9439  elfz2nn0  9459  difelfzle  9476  1fv  9481  4fvwrd4  9482  fzo1fzo0n0  9525  elfzom1elp1fzo  9544  subfzo0  9584  qtri3or  9585  adddivflid  9630  flltdivnn0lt  9642  intfracq  9658  modqid2  9689  modfzo0difsn  9733  iseqvalt  9793  iseqf1olemqcl  9823  iseqf1olemnab  9825  iseqf1olemab  9826  iseqf1olemmo  9829  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  expclzaplem  9881  leexp1a  9912  expubnd  9914  le2sq2  9932  sumsqeq0  9935  bernneq  9974  expnlbnd  9978  nn0opthd  10030  faclbnd6  10052  facavg  10054  iseqcoll  10147  shftlem  10150  shftfvalg  10152  shftfval  10155  cvg1nlemcau  10316  cvg1nlemres  10317  rexuz3  10322  resqrexlemcvg  10351  resqrexlemglsq  10354  resqrexlemga  10355  sqrtle  10368  sqrtlt  10369  sqrt11  10371  sqrtsq2  10375  absmul  10401  sqabs  10414  abslt  10420  absle  10421  lenegsq  10427  maxleastb  10546  maxltsup  10550  rexanre  10552  negfi  10557  climcn2  10595  mulcn2  10598  isummolem2a  10665  isummo  10667  fisum  10670  fisumcvg3  10679  fsumcl2lem  10680  fsumadd  10688  dvdsval3  10706  dvdscmul  10729  dvdsmulc  10730  dvdscmulr  10731  dvdsmulcr  10732  modmulconst  10734  dvds2ln  10735  ltoddhalfle  10799  nn0o  10813  divalg2  10832  ndvdssub  10836  ndvdsadd  10837  infssuzex  10851  divgcdz  10869  gcd0id  10876  gcdaddm  10881  bezoutlemstep  10892  bezoutlemmain  10893  dfgcd3  10905  dfgcd2  10909  lcmcllem  10955  dvdslcm  10957  lcmgcdlem  10965  lcmgcdnn  10970  qredeq  10984  qredeu  10985  rpdvds  10987  divgcdcoprm0  10989  cncongr1  10991  cncongr2  10992  cncongrcoprm  10994  prmind2  11008  isprm6  11032  prmexpb  11036  cncongrprm  11042  sqrt2irrlem  11046  pw2dvdslemn  11049  oddpwdclemxy  11053  oddpwdclemdc  11057  oddpwdc  11058  hashdvds  11103  hashgcdlem  11109  bdop  11235  bdunexb  11280  bj-om  11301  findset  11309  bj-peano4  11319  bj-inf2vn  11338  bj-inf2vn2  11339  nninfalllemn  11367  qdencn  11384