ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jca Unicode version

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
StepHypRef Expression
1 jca.1 . 2  |-  ( ph  ->  ps )
2 jca.2 . 2  |-  ( ph  ->  ch )
3 pm3.2 138 . 2  |-  ( ps 
->  ( ch  ->  ( ps  /\  ch ) ) )
41, 2, 3sylc 62 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
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  413  jcab  577  ioran  726  ordi  790  stdcndc  815  stdcndcOLD  816  dfandc  854  pm4.55dc  907  mpbi2and  912  mpbir2and  913  pm4.82  919  pm4.83dc  920  rnlem  945  syl22anc  1202  syl112anc  1205  syl121anc  1206  syl211anc  1207  syl23anc  1208  syl32anc  1209  syl122anc  1210  syl212anc  1211  syl221anc  1212  syl222anc  1217  syl123anc  1218  syl132anc  1219  syl213anc  1220  syl231anc  1221  syl312anc  1222  syl321anc  1223  syl223anc  1227  syl232anc  1228  syl322anc  1229  syl233anc  1230  syl323anc  1231  syl332anc  1232  ecased  1312  19.26  1442  nfand  1532  19.40  1595  equsexd  1692  sbcof2  1766  sbequ8  1803  eu2  2021  eu3h  2022  eu5  2024  mooran2  2050  datisi  2087  felapton  2091  darapti  2092  dimatis  2094  fresison  2095  fesapo  2097  reximssdv  2513  r19.26  2535  r19.29af2  2549  r19.40  2562  eqvinc  2782  eqvincg  2783  elrabd  2815  reu6  2846  reu3  2847  indifdir  3302  undif3ss  3307  un00  3379  eqifdc  3476  disjpr2  3557  prel12  3668  prneimg  3671  preqsn  3672  disjiun  3894  opth  4129  0nelop  4140  euotd  4146  opelopabsb  4152  ispod  4196  elon2  4268  unexb  4333  opeluu  4341  eusvnfb  4345  suc11g  4442  nlimsucg  4451  tfi  4466  vtoclr  4557  opthprc  4560  ideqg  4660  resiexg  4834  dminss  4923  imainss  4924  ssxpbm  4944  relrelss  5035  funopg  5127  fntpg  5149  fun11uni  5163  imain  5175  funimaexglem  5176  funssxp  5262  ffdm  5263  f00  5284  dffo2  5319  fodmrnu  5323  foco  5325  fun11iun  5356  f1o00  5370  fsnd  5378  fv3  5412  dff2  5532  dff3im  5533  dffo4  5536  ffnfv  5546  ffvresb  5551  fsn2  5562  fconstfvm  5606  fnfvima  5620  fcof1o  5658  isocnv  5680  isotr  5685  riotaprop  5721  acexmidlemcase  5737  caovlem2d  5931  f1ocnvd  5940  caofcom  5973  resfunexgALT  5976  elxp7  6036  2ndrn  6049  1stconst  6086  2ndconst  6087  cnvf1olem  6089  poxp  6097  dftpos4  6128  dfsmo2  6152  tfrlem5  6179  tfrlemiex  6196  tfr1onlemsucaccv  6206  tfr1onlembfn  6209  tfr1onlemex  6212  tfr1onlemres  6214  tfrcllemsucaccv  6219  tfrcllembfn  6222  tfrcllemex  6225  tfrcllemres  6227  tfrcl  6229  frecabex  6263  frecabcl  6264  frecfcllem  6269  frecrdg  6273  oawordi  6333  nntri3  6361  nntr2  6367  nnmordi  6380  iserd  6423  relelec  6437  erth  6441  qliftfun  6479  mapsncnv  6557  mptelixpg  6596  bren  6609  findcard2d  6753  findcard2sd  6754  isinfinf  6759  tridc  6761  nnwetri  6772  undifdcss  6779  fiintim  6785  fisseneq  6788  fidcenumlemim  6808  sbthlemi9  6821  supisolem  6863  ordiso2  6888  updjud  6935  difinfsn  6953  ctssdccl  6964  acfun  7031  ccfunen  7047  elni2  7090  dfplpq2  7130  dfmpq2  7131  enqbreq2  7133  enqdc1  7138  addcmpblnq  7143  addclnq  7151  nqpi  7154  addassnqg  7158  mulassnqg  7160  mulcanenq  7161  distrnqg  7163  1qec  7164  recexnq  7166  subhalfnqq  7190  enq0tr  7210  nqnq0pi  7214  nq0nn  7218  mulcanenq0ec  7221  nnnq0lem1  7222  addclnq0  7227  distrnq0  7235  addassnq0lemcl  7237  elnp1st2nd  7252  prarloc  7279  addlocprlemlt  7307  addlocprlemeq  7309  addlocprlemgt  7310  addclpr  7313  nqprm  7318  mullocprlem  7346  mullocpr  7347  mulclpr  7348  ltpopr  7371  ltaddpr  7373  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemrnd  7381  ltexprlemdisj  7382  addcanprleml  7390  addcanprlemu  7391  addcanprg  7392  recexprlemm  7400  recexprlemopl  7401  recexprlemopu  7403  recexprlemrnd  7405  recexprlemdisj  7406  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemopu  7424  cauappcvgprlemrnd  7426  cauappcvgprlemdisj  7427  cauappcvgprlemlim  7437  caucvgprlemnkj  7442  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemopu  7447  caucvgprlemrnd  7449  caucvgprlemlim  7457  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemnjltk  7467  caucvgprprlemm  7472  caucvgprprlemopl  7473  caucvgprprlemopu  7475  caucvgprprlemrnd  7477  caucvgprprlemexbt  7482  caucvgprprlemlim  7487  suplocexprlemrl  7493  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemex  7498  suplocexprlemub  7499  prsrlem1  7518  mulclsr  7530  mulasssrg  7534  distrsrg  7535  suplocsrlemb  7582  elreal2  7606  axmulass  7649  axdistr  7650  axcaucvglemcau  7674  add20  8204  mullt0  8210  rereim  8316  ltmul1  8322  cru  8332  mulap0r  8345  aprcl  8376  divmuldivap  8440  divmuleqap  8445  divadddivap  8455  divmuldivapd  8560  div2subap  8564  ltmul12a  8586  lemul12a  8588  lemulge11  8592  lediv12a  8620  lediv2a  8621  recgt1i  8624  recreclt  8626  ledivp1  8629  lemul1ad  8665  lemul2ad  8666  ltmul12ad  8667  lemul12ad  8668  lemul12bd  8669  nndivre  8724  nndivtr  8730  halfaddsubcl  8921  halfaddsub  8922  lt2halves  8923  nnrecl  8943  elnn0nn  8987  elnnnn0b  8989  elnnnn0c  8990  nn0addge1  8991  nn0addge2  8992  xnn0xrnemnf  9020  elnn0z  9035  elnnz1  9045  nzadd  9074  elz2  9090  zdivadd  9108  zdivmul  9109  zextle  9110  peano2uz2  9126  uzind  9130  btwnz  9138  uzss  9314  eluzp1m1  9317  eluz2b2  9365  qre  9385  qaddcl  9395  qmulcl  9397  qreccl  9402  irradd  9406  irrmul  9407  cnref1o  9408  rprege0  9424  rprene0  9427  rpreap0  9428  rpcnne0  9429  rpcnap0  9430  rpregt0d  9458  rprege0d  9459  rprene0d  9460  rpcnne0d  9461  lediv2ad  9474  ledivge1le  9481  lediv12ad  9511  nnledivrp  9521  nn0ledivnn  9522  xrlttri3  9551  xrrebnd  9570  xrrege0  9576  xnn0xadd0  9618  xlesubadd  9634  elioo4g  9685  ioomax  9699  iccmax  9700  divelunit  9753  elfz5  9766  uzsubsubfz  9795  fzopth  9809  fzass4  9810  fzrev2  9833  uzsplit  9840  elfz2nn0  9860  difelfzle  9879  1fv  9884  4fvwrd4  9885  fzo1fzo0n0  9928  elfzom1elp1fzo  9947  subfzo0  9987  qtri3or  9988  adddivflid  10033  flltdivnn0lt  10045  intfracq  10061  modqid2  10092  modfzo0difsn  10136  seq3val  10199  seqvalcd  10200  iseqf1olemqcl  10227  iseqf1olemnab  10229  iseqf1olemab  10230  iseqf1olemmo  10233  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  expclzaplem  10285  leexp1a  10316  expubnd  10318  le2sq2  10336  sumsqeq0  10339  bernneq  10380  expnlbnd  10384  nn0opthd  10436  faclbnd6  10458  facavg  10460  seq3coll  10553  shftlem  10556  shftfvalg  10558  shftfval  10561  cvg1nlemcau  10724  cvg1nlemres  10725  rexuz3  10730  resqrexlemcvg  10759  resqrexlemglsq  10762  resqrexlemga  10763  sqrtle  10776  sqrtlt  10777  sqrt11  10779  sqrtsq2  10783  absmul  10809  sqabs  10822  abslt  10828  absle  10829  lenegsq  10835  maxleastb  10954  maxltsup  10958  rexanre  10960  negfi  10967  xrmaxiflemab  10984  xrmaxiflemlub  10985  xrmaxltsup  10995  xrmaxadd  10998  climcn2  11046  mulcn2  11049  summodclem2a  11118  summodc  11120  fsum3  11124  fsum3cvg3  11133  fsumcl2lem  11135  fsumadd  11143  fsump1i  11170  fsum0diaglem  11177  mptfzshft  11179  fsumrev  11180  fsummulc2  11185  fsum00  11199  expcnvap0  11239  mertenslemi1  11272  eftlub  11323  efieq  11369  sincos1sgn  11398  demoivreALT  11407  dvdsval3  11424  dvdscmul  11447  dvdsmulc  11448  dvdscmulr  11449  dvdsmulcr  11450  modmulconst  11452  dvds2ln  11453  ltoddhalfle  11517  nn0o  11531  divalg2  11550  ndvdssub  11554  ndvdsadd  11555  infssuzex  11569  divgcdz  11587  gcd0id  11594  gcdaddm  11599  bezoutlemstep  11612  bezoutlemmain  11613  dfgcd3  11625  dfgcd2  11629  lcmcllem  11675  dvdslcm  11677  lcmgcdlem  11685  lcmgcdnn  11690  qredeq  11704  qredeu  11705  rpdvds  11707  divgcdcoprm0  11709  cncongr1  11711  cncongr2  11712  cncongrcoprm  11714  prmind2  11728  isprm6  11752  prmexpb  11756  cncongrprm  11762  sqrt2irrlem  11766  pw2dvdslemn  11770  oddpwdclemxy  11774  oddpwdclemdc  11778  oddpwdc  11779  hashdvds  11824  hashgcdlem  11830  ennnfonelemfun  11857  ennnfonelemim  11864  ctinfomlemom  11867  ctinfom  11868  ctinf  11870  ctiunctlemfo  11879  topgele  12123  tgcl  12160  epttop  12186  opnssneib  12252  iscnp4  12314  cnco  12317  cncnp  12326  cnrest2  12332  lmss  12342  txcnp  12367  txcn  12371  cnmpt12  12383  cnmpt22  12390  hmeof1o  12405  psmetres2  12429  distspace  12431  ismeti  12442  isxmetd  12443  xmetpsmet  12465  xblss2ps  12500  xblss2  12501  blcntrps  12511  blcntr  12512  blin2  12528  mopni3  12580  metequiv2  12592  bdmet  12598  xmettx  12606  cnbl0  12630  cnblcld  12631  tgioo  12642  elcncf1di  12662  dedekindeulemlu  12695  suplociccex  12699  dedekindicclemlu  12704  dedekindicc  12707  ivthinclemlopn  12710  ivthdec  12718  cnplimcim  12732  limccnp2lem  12741  dvfvalap  12746  sin0pilem1  12789  pilem3  12791  ptolemy  12832  sincosq1sgn  12834  sinq12gt0  12838  bj-nnan  12875  bdop  13000  bdunexb  13045  bj-om  13062  findset  13070  bj-peano4  13080  bj-inf2vn  13099  bj-inf2vn2  13100  pwle2  13120  pwf1oexmid  13121  nninfalllemn  13129  sbthom  13148  qdencn  13149  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator