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

Theorem jca 294
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 130 . 2  |-  ( ps 
->  ( ch  ->  ( ps  /\  ch ) ) )
41, 2, 3sylc 60 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  jca31  296  jca32  297  jcai  298  jctil  299  jctir  300  ancli  310  ancri  311  sylanbrc  402  jcab  545  ioran  679  ordi  740  dfandc  789  stabtestimpdc  835  pm4.55dc  857  mpbi2and  861  mpbir2and  862  pm4.82  868  pm4.83dc  869  rnlem  894  syl22anc  1147  syl112anc  1150  syl121anc  1151  syl211anc  1152  syl23anc  1153  syl32anc  1154  syl122anc  1155  syl212anc  1156  syl221anc  1157  syl222anc  1162  syl123anc  1163  syl132anc  1164  syl213anc  1165  syl231anc  1166  syl312anc  1167  syl321anc  1168  syl223anc  1172  syl232anc  1173  syl322anc  1174  syl233anc  1175  syl323anc  1176  syl332anc  1177  ecased  1255  19.26  1386  nfand  1476  19.40  1538  equsexd  1633  sbcof2  1707  sbequ8  1743  eu2  1960  eu3h  1961  eu5  1963  mooran2  1989  datisi  2026  felapton  2030  darapti  2031  dimatis  2033  fresison  2034  fesapo  2036  r19.26  2458  r19.29af2  2469  r19.40  2481  eqvinc  2689  eqvincg  2690  reu6  2752  reu3  2753  indifdir  3220  undif3ss  3225  un00  3290  disjpr2  3461  prel12  3569  prneimg  3572  preqsn  3573  opexgOLD  3992  opth  4001  0nelop  4012  euotd  4018  opelopabsb  4024  ispod  4068  elon2  4140  unexb  4204  opeluu  4209  eusvnfb  4213  suc11g  4308  nlimsucg  4317  tfi  4332  vtoclr  4415  opthprc  4418  ideqg  4514  resiexg  4680  dminss  4765  imainss  4766  ssxpbm  4783  relrelss  4871  funopg  4961  fntpg  4982  fun11uni  4996  imain  5008  funimaexglem  5009  funssxp  5087  ffdm  5088  f00  5108  dffo2  5137  fodmrnu  5141  foco  5143  fun11iun  5174  f1o00  5188  fv3  5224  dff2  5338  dff3im  5339  dffo4  5342  ffnfv  5350  ffvresb  5355  fsn2  5364  fconstfvm  5406  fnfvima  5420  fcof1o  5456  isocnv  5478  isotr  5483  riotaprop  5518  acexmidlemcase  5534  caovlem2d  5720  f1ocnvd  5729  caofcom  5761  resfunexgALT  5764  elxp7  5824  2ndrn  5836  1stconst  5869  2ndconst  5870  cnvf1olem  5872  poxp  5880  dftpos4  5908  dfsmo2  5932  tfrlem5  5960  tfrlemiex  5975  rdgon  6003  frecabex  6014  frecrdg  6022  oawordi  6079  nntri3  6105  nnmordi  6119  iserd  6162  relelec  6176  erth  6180  qliftfun  6218  bren  6258  findcard2d  6378  findcard2sd  6379  nnwetri  6384  supisolem  6411  ordiso2  6414  elni2  6469  dfplpq2  6509  dfmpq2  6510  enqbreq2  6512  enqdc1  6517  addcmpblnq  6522  addclnq  6530  nqpi  6533  addassnqg  6537  mulassnqg  6539  mulcanenq  6540  distrnqg  6542  1qec  6543  recexnq  6545  subhalfnqq  6569  enq0tr  6589  nqnq0pi  6593  nq0nn  6597  mulcanenq0ec  6600  nnnq0lem1  6601  addclnq0  6606  distrnq0  6614  addassnq0lemcl  6616  elnp1st2nd  6631  prarloc  6658  addlocprlemlt  6686  addlocprlemeq  6688  addlocprlemgt  6689  addclpr  6692  nqprm  6697  mullocprlem  6725  mullocpr  6726  mulclpr  6727  ltpopr  6750  ltaddpr  6752  ltexprlemm  6755  ltexprlemopl  6756  ltexprlemopu  6758  ltexprlemrnd  6760  ltexprlemdisj  6761  addcanprleml  6769  addcanprlemu  6770  addcanprg  6771  recexprlemm  6779  recexprlemopl  6780  recexprlemopu  6782  recexprlemrnd  6784  recexprlemdisj  6785  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemopu  6803  cauappcvgprlemrnd  6805  cauappcvgprlemdisj  6806  cauappcvgprlemlim  6816  caucvgprlemnkj  6821  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemopu  6826  caucvgprlemrnd  6828  caucvgprlemlim  6836  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemnjltk  6846  caucvgprprlemm  6851  caucvgprprlemopl  6852  caucvgprprlemopu  6854  caucvgprprlemrnd  6856  caucvgprprlemexbt  6861  caucvgprprlemlim  6866  prsrlem1  6884  mulclsr  6896  mulasssrg  6900  distrsrg  6901  elreal2  6964  axmulass  7004  axdistr  7005  axcaucvglemcau  7029  add20  7542  mullt0  7548  rereim  7650  ltmul1  7656  cru  7666  mulap0r  7679  divmuldivap  7762  divmuleqap  7767  divadddivap  7777  divmuldivapd  7880  ltmul12a  7900  lemul12a  7902  lemulge11  7906  lediv12a  7934  lediv2a  7935  recgt1i  7938  recreclt  7940  ledivp1  7943  lemul1ad  7979  lemul2ad  7980  ltmul12ad  7981  lemul12ad  7982  lemul12bd  7983  nndivre  8024  nndivtr  8030  halfaddsubcl  8214  halfaddsub  8215  lt2halves  8216  nnrecl  8236  elnn0nn  8280  elnnnn0b  8282  elnnnn0c  8283  nn0addge1  8284  nn0addge2  8285  elnn0z  8314  elnnz1  8324  nzadd  8353  elz2  8369  zdivadd  8386  zdivmul  8387  zextle  8388  peano2uz2  8403  uzind  8407  btwnz  8415  uzss  8588  eluzp1m1  8591  eluz2b2  8636  qre  8656  qaddcl  8666  qmulcl  8668  qreccl  8673  irradd  8677  irrmul  8678  cnref1o  8679  rprege0  8694  rprene0  8697  rpreap0  8698  rpcnne0  8699  rpcnap0  8700  rpregt0d  8726  rprege0d  8727  rprene0d  8728  rpcnne0d  8729  lediv2ad  8742  ledivge1le  8749  lediv12ad  8779  nnledivrp  8783  nn0ledivnn  8784  xrlttri3  8818  xrrebnd  8832  xrrege0  8838  elioo4g  8903  ioomax  8917  iccmax  8918  divelunit  8970  elfz5  8983  uzsubsubfz  9012  fzopth  9025  fzass4  9026  fzrev2  9048  uzsplit  9055  elfz2nn0  9074  difelfzle  9093  1fv  9097  4fvwrd4  9098  fzo1fzo0n0  9140  elfzom1elp1fzo  9159  subfzo0  9198  qtri3or  9199  adddivflid  9241  flltdivnn0lt  9253  intfracq  9269  modqid2  9300  modfzo0difsn  9344  expclzaplem  9443  leexp1a  9474  expubnd  9476  le2sq2  9494  sumsqeq0  9497  bernneq  9536  expnlbnd  9540  nn0opthd  9589  faclbnd6  9611  facavg  9613  shftlem  9644  shftfvalg  9646  shftfval  9649  cvg1nlemcau  9810  cvg1nlemres  9811  rexuz3  9816  resqrexlemcvg  9845  resqrexlemglsq  9848  resqrexlemga  9849  sqrtle  9862  sqrtlt  9863  sqrt11  9865  sqrtsq2  9869  absmul  9895  sqabs  9908  abslt  9914  absle  9915  lenegsq  9921  climcn2  10060  mulcn2  10063  dvdsval3  10111  dvdscmul  10133  dvdsmulc  10134  dvdscmulr  10135  dvdsmulcr  10136  modmulconst  10138  dvds2ln  10139  ltoddhalfle  10204  nn0o  10218  sqr2irrlem  10229  pw2dvdslemn  10232  oddpwdclemxy  10236  oddpwdclemdc  10240  oddpwdc  10241  bdop  10361  bdunexb  10406  bj-om  10427  findset  10436  bj-peano4  10446  bj-inf2vn  10465  bj-inf2vn2  10466  qdencn  10490
  Copyright terms: Public domain W3C validator