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

Theorem jca 290
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
jca.2
Assertion
Ref Expression
jca

Proof of Theorem jca
StepHypRef Expression
1 jca.1 . 2
2 jca.2 . 2
3 pm3.2 126 . 2
41, 2, 3sylc 56 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  jca31  292  jca32  293  jcai  294  jctil  295  jctir  296  ancli  306  ancri  307  sylanbrc  394  jcab  535  ioran  668  ordi  728  dfandc  777  stabtestimpdc  823  pm4.55dc  845  mpbi2and  849  mpbir2and  850  pm4.82  856  pm4.83dc  857  rnlem  882  syl22anc  1135  syl112anc  1138  syl121anc  1139  syl211anc  1140  syl23anc  1141  syl32anc  1142  syl122anc  1143  syl212anc  1144  syl221anc  1145  syl222anc  1150  syl123anc  1151  syl132anc  1152  syl213anc  1153  syl231anc  1154  syl312anc  1155  syl321anc  1156  syl223anc  1160  syl232anc  1161  syl322anc  1162  syl233anc  1163  syl323anc  1164  syl332anc  1165  ecased  1238  19.26  1367  nfand  1457  19.40  1519  equsexd  1614  sbcof2  1688  sbequ8  1724  eu2  1941  eu3h  1942  eu5  1944  mooran2  1970  datisi  2007  felapton  2011  darapti  2012  dimatis  2014  fresison  2015  fesapo  2017  r19.26  2435  r19.29af2  2446  r19.40  2458  eqvinc  2661  eqvincg  2662  reu6  2724  reu3  2725  indifdir  3187  undif3ss  3192  un00  3257  disjpr2  3425  prel12  3533  prneimg  3536  preqsn  3537  opexgOLD  3956  opth  3965  0nelop  3976  euotd  3982  opelopabsb  3988  ispod  4032  elon2  4079  unexb  4143  opeluu  4148  eusvnfb  4152  suc11g  4235  nlimsucg  4242  tfi  4248  vtoclr  4331  opthprc  4334  ideqg  4430  resiexg  4596  dminss  4681  imainss  4682  ssxpbm  4699  relrelss  4787  funopg  4877  fntpg  4898  fun11uni  4912  imain  4924  funimaexglem  4925  funssxp  5003  ffdm  5004  f00  5024  dffo2  5053  fodmrnu  5057  foco  5059  fun11iun  5090  f1o00  5104  fv3  5140  dff2  5254  dff3im  5255  dffo4  5258  ffnfv  5266  ffvresb  5271  fsn2  5280  fconstfvm  5322  fnfvima  5336  fcof1o  5372  isocnv  5394  isotr  5399  riotaprop  5434  acexmidlemcase  5450  caovlem2d  5635  f1ocnvd  5644  caofcom  5676  resfunexgALT  5679  elxp7  5739  2ndrn  5751  1stconst  5784  2ndconst  5785  cnvf1olem  5787  poxp  5794  dftpos4  5819  dfsmo2  5843  tfrlem5  5871  tfrlemiex  5886  rdgon  5913  frecabex  5923  frecrdg  5931  oawordi  5988  nntri3  6014  nnmordi  6025  iserd  6068  relelec  6082  erth  6086  qliftfun  6124  bren  6164  elni2  6298  dfplpq2  6338  dfmpq2  6339  enqbreq2  6341  enqdc1  6346  addcmpblnq  6351  addclnq  6359  nqpi  6362  addassnqg  6366  mulassnqg  6368  mulcanenq  6369  distrnqg  6371  1qec  6372  recexnq  6374  subhalfnqq  6397  enq0tr  6417  nqnq0pi  6421  nq0nn  6425  mulcanenq0ec  6428  nnnq0lem1  6429  addclnq0  6434  distrnq0  6442  addassnq0lemcl  6444  elnp1st2nd  6459  prarloc  6486  addlocprlemlt  6514  addlocprlemeq  6516  addlocprlemgt  6517  addclpr  6520  nqprm  6525  mullocprlem  6551  mullocpr  6552  mulclpr  6553  ltpopr  6569  ltaddpr  6571  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemrnd  6579  ltexprlemdisj  6580  addcanprleml  6588  addcanprlemu  6589  addcanprg  6590  recexprlemm  6596  recexprlemopl  6597  recexprlemopu  6599  recexprlemrnd  6601  recexprlemdisj  6602  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemrnd  6622  cauappcvgprlemdisj  6623  cauappcvgprlemlim  6633  caucvgprlemnkj  6637  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemrnd  6644  caucvgprlemlim  6652  prsrlem1  6670  mulclsr  6682  mulasssrg  6686  distrsrg  6687  elreal2  6728  axmulass  6757  axdistr  6758  add20  7264  mullt0  7270  rereim  7370  ltmul1  7376  cru  7386  mulap0r  7399  divmuldivap  7470  divmuleqap  7475  divadddivap  7485  ltmul12a  7607  lemul12a  7609  lemulge11  7613  lediv12a  7641  lediv2a  7642  recgt1i  7645  recreclt  7647  ledivp1  7650  lemul1ad  7686  lemul2ad  7687  ltmul12ad  7688  lemul12ad  7689  lemul12bd  7690  nndivre  7730  nndivtr  7736  halfaddsubcl  7935  halfaddsub  7936  lt2halves  7937  nnrecl  7955  elnn0nn  8000  elnnnn0b  8002  elnnnn0c  8003  nn0addge1  8004  nn0addge2  8005  elnn0z  8034  elnnz1  8044  elz2  8088  zdivadd  8105  zdivmul  8106  zextle  8107  peano2uz2  8121  uzind  8125  btwnz  8133  uzss  8269  eluzp1m1  8272  eluz2b2  8316  qre  8336  qaddcl  8346  qmulcl  8348  qreccl  8351  irradd  8355  irrmul  8356  cnref1o  8357  rprege0  8372  rprene0  8375  rpreap0  8376  rpcnne0  8377  rpcnap0  8378  rpregt0d  8403  rprege0d  8404  rprene0d  8405  rpcnne0d  8406  lediv2ad  8419  lediv12ad  8452  xrlttri3  8488  xrrebnd  8502  xrrege0  8508  elioo4g  8573  ioomax  8587  iccmax  8588  divelunit  8640  elfz5  8652  uzsubsubfz  8681  fzopth  8694  fzass4  8695  fzrev2  8717  uzsplit  8724  elfz2nn0  8743  difelfzle  8762  1fv  8766  4fvwrd4  8767  fzo1fzo0n0  8809  elfzom1elp1fzo  8828  expclzaplem  8933  leexp1a  8963  expubnd  8965  le2sq2  8982  sumsqeq0  8985  bernneq  9022  expnlbnd  9026  bdop  9330  bdunexb  9375  bj-om  9396  findset  9405  bj-peano4  9415  bj-inf2vn  9434  bj-inf2vn2  9435
  Copyright terms: Public domain W3C validator