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

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 (𝜑𝜓)
jca.2 (𝜑𝜒)
Assertion
Ref Expression
jca (𝜑 → (𝜓𝜒))

Proof of Theorem jca
StepHypRef Expression
1 jca.1 . 2 (𝜑𝜓)
2 jca.2 . 2 (𝜑𝜒)
3 pm3.2 137 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 61 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
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  1658  sbcof2  1732  sbequ8  1769  eu2  1986  eu3h  1987  eu5  1989  mooran2  2015  datisi  2052  felapton  2056  darapti  2057  dimatis  2059  fresison  2060  fesapo  2062  r19.26  2486  r19.29af2  2497  r19.40  2509  eqvinc  2719  eqvincg  2720  reu6  2782  reu3  2783  indifdir  3227  undif3ss  3232  un00  3297  disjpr2  3464  prel12  3571  prneimg  3574  preqsn  3575  opth  4000  0nelop  4011  euotd  4017  opelopabsb  4023  ispod  4067  elon2  4139  unexb  4203  opeluu  4208  eusvnfb  4212  suc11g  4308  nlimsucg  4317  tfi  4331  vtoclr  4414  opthprc  4417  ideqg  4515  resiexg  4683  dminss  4768  imainss  4769  ssxpbm  4786  relrelss  4874  funopg  4964  fntpg  4986  fun11uni  5000  imain  5012  funimaexglem  5013  funssxp  5091  ffdm  5092  f00  5112  dffo2  5141  fodmrnu  5145  foco  5147  fun11iun  5178  f1o00  5192  fv3  5229  dff2  5343  dff3im  5344  dffo4  5347  ffnfv  5355  ffvresb  5360  fsn2  5369  fconstfvm  5411  fnfvima  5425  fcof1o  5460  isocnv  5482  isotr  5487  riotaprop  5522  acexmidlemcase  5538  caovlem2d  5724  f1ocnvd  5733  caofcom  5765  resfunexgALT  5768  elxp7  5828  2ndrn  5840  1stconst  5873  2ndconst  5874  cnvf1olem  5876  poxp  5884  dftpos4  5912  dfsmo2  5936  tfrlem5  5963  tfrlemiex  5980  tfr1onlemsucaccv  5990  tfr1onlembfn  5993  tfr1onlemex  5996  tfr1onlemres  5998  tfrcllemsucaccv  6003  tfrcllembfn  6006  tfrcllemex  6009  tfrcllemres  6011  tfrcl  6013  frecabex  6047  frecabcl  6048  frecfcllem  6053  frecrdg  6057  oawordi  6113  nntri3  6141  nnmordi  6155  iserd  6198  relelec  6212  erth  6216  qliftfun  6254  bren  6294  findcard2d  6425  findcard2sd  6426  nnwetri  6436  supisolem  6480  ordiso2  6505  elni2  6566  dfplpq2  6606  dfmpq2  6607  enqbreq2  6609  enqdc1  6614  addcmpblnq  6619  addclnq  6627  nqpi  6630  addassnqg  6634  mulassnqg  6636  mulcanenq  6637  distrnqg  6639  1qec  6640  recexnq  6642  subhalfnqq  6666  enq0tr  6686  nqnq0pi  6690  nq0nn  6694  mulcanenq0ec  6697  nnnq0lem1  6698  addclnq0  6703  distrnq0  6711  addassnq0lemcl  6713  elnp1st2nd  6728  prarloc  6755  addlocprlemlt  6783  addlocprlemeq  6785  addlocprlemgt  6786  addclpr  6789  nqprm  6794  mullocprlem  6822  mullocpr  6823  mulclpr  6824  ltpopr  6847  ltaddpr  6849  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemrnd  6857  ltexprlemdisj  6858  addcanprleml  6866  addcanprlemu  6867  addcanprg  6868  recexprlemm  6876  recexprlemopl  6877  recexprlemopu  6879  recexprlemrnd  6881  recexprlemdisj  6882  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemopu  6900  cauappcvgprlemrnd  6902  cauappcvgprlemdisj  6903  cauappcvgprlemlim  6913  caucvgprlemnkj  6918  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemopu  6923  caucvgprlemrnd  6925  caucvgprlemlim  6933  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnjltk  6943  caucvgprprlemm  6948  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemrnd  6953  caucvgprprlemexbt  6958  caucvgprprlemlim  6963  prsrlem1  6981  mulclsr  6993  mulasssrg  6997  distrsrg  6998  elreal2  7061  axmulass  7101  axdistr  7102  axcaucvglemcau  7126  add20  7645  mullt0  7651  rereim  7753  ltmul1  7759  cru  7769  mulap0r  7782  divmuldivap  7867  divmuleqap  7872  divadddivap  7882  divmuldivapd  7985  ltmul12a  8005  lemul12a  8007  lemulge11  8011  lediv12a  8039  lediv2a  8040  recgt1i  8043  recreclt  8045  ledivp1  8048  lemul1ad  8084  lemul2ad  8085  ltmul12ad  8086  lemul12ad  8087  lemul12bd  8088  nndivre  8141  nndivtr  8147  halfaddsubcl  8331  halfaddsub  8332  lt2halves  8333  nnrecl  8353  elnn0nn  8397  elnnnn0b  8399  elnnnn0c  8400  nn0addge1  8401  nn0addge2  8402  xnn0xrnemnf  8430  elnn0z  8445  elnnz1  8455  nzadd  8484  elz2  8500  zdivadd  8517  zdivmul  8518  zextle  8519  peano2uz2  8535  uzind  8539  btwnz  8547  uzss  8720  eluzp1m1  8723  eluz2b2  8771  qre  8791  qaddcl  8801  qmulcl  8803  qreccl  8808  irradd  8812  irrmul  8813  cnref1o  8814  rprege0  8829  rprene0  8832  rpreap0  8833  rpcnne0  8834  rpcnap0  8835  rpregt0d  8861  rprege0d  8862  rprene0d  8863  rpcnne0d  8864  lediv2ad  8877  ledivge1le  8884  lediv12ad  8914  nnledivrp  8918  nn0ledivnn  8919  xrlttri3  8948  xrrebnd  8962  xrrege0  8968  elioo4g  9033  ioomax  9047  iccmax  9048  divelunit  9100  elfz5  9113  uzsubsubfz  9142  fzopth  9155  fzass4  9156  fzrev2  9178  uzsplit  9185  elfz2nn0  9205  difelfzle  9222  1fv  9226  4fvwrd4  9227  fzo1fzo0n0  9269  elfzom1elp1fzo  9288  subfzo0  9328  qtri3or  9329  adddivflid  9374  flltdivnn0lt  9386  intfracq  9402  modqid2  9433  modfzo0difsn  9477  iseqvalt  9532  expclzaplem  9597  leexp1a  9628  expubnd  9630  le2sq2  9648  sumsqeq0  9651  bernneq  9690  expnlbnd  9694  nn0opthd  9746  faclbnd6  9768  facavg  9770  shftlem  9842  shftfvalg  9844  shftfval  9847  cvg1nlemcau  10008  cvg1nlemres  10009  rexuz3  10014  resqrexlemcvg  10043  resqrexlemglsq  10046  resqrexlemga  10047  sqrtle  10060  sqrtlt  10061  sqrt11  10063  sqrtsq2  10067  absmul  10093  sqabs  10106  abslt  10112  absle  10113  lenegsq  10119  maxleastb  10238  maxltsup  10242  rexanre  10244  negfi  10248  climcn2  10286  mulcn2  10289  dvdsval3  10344  dvdscmul  10367  dvdsmulc  10368  dvdscmulr  10369  dvdsmulcr  10370  modmulconst  10372  dvds2ln  10373  ltoddhalfle  10437  nn0o  10451  divalg2  10470  ndvdssub  10474  ndvdsadd  10475  infssuzex  10489  divgcdz  10507  gcd0id  10514  gcdaddm  10519  bezoutlemstep  10530  bezoutlemmain  10531  dfgcd3  10543  dfgcd2  10547  lcmcllem  10593  dvdslcm  10595  lcmgcdlem  10603  lcmgcdnn  10608  qredeq  10622  qredeu  10623  rpdvds  10625  divgcdcoprm0  10627  cncongr1  10629  cncongr2  10630  cncongrcoprm  10632  prmind2  10646  isprm6  10670  prmexpb  10674  cncongrprm  10680  sqrt2irrlem  10684  pw2dvdslemn  10687  oddpwdclemxy  10691  oddpwdclemdc  10695  oddpwdc  10696  bdop  10824  bdunexb  10869  bj-om  10890  findset  10898  bj-peano4  10908  bj-inf2vn  10927  bj-inf2vn2  10928  qdencn  10943
  Copyright terms: Public domain W3C validator