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  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  3489  prel12  3598  prneimg  3601  preqsn  3602  opth  4038  0nelop  4049  euotd  4055  opelopabsb  4061  ispod  4105  elon2  4177  unexb  4241  opeluu  4246  eusvnfb  4250  suc11g  4346  nlimsucg  4355  tfi  4370  vtoclr  4454  opthprc  4457  ideqg  4555  resiexg  4724  dminss  4812  imainss  4813  ssxpbm  4832  relrelss  4923  funopg  5013  fntpg  5035  fun11uni  5049  imain  5061  funimaexglem  5062  funssxp  5144  ffdm  5145  f00  5165  dffo2  5200  fodmrnu  5204  foco  5206  fun11iun  5237  f1o00  5251  fv3  5291  dff2  5406  dff3im  5407  dffo4  5410  ffnfv  5419  ffvresb  5424  fsn2  5434  fconstfvm  5476  fnfvima  5490  fcof1o  5529  isocnv  5551  isotr  5556  riotaprop  5592  acexmidlemcase  5608  caovlem2d  5794  f1ocnvd  5803  caofcom  5835  resfunexgALT  5838  elxp7  5898  2ndrn  5910  1stconst  5943  2ndconst  5944  cnvf1olem  5946  poxp  5954  dftpos4  5982  dfsmo2  6006  tfrlem5  6033  tfrlemiex  6050  tfr1onlemsucaccv  6060  tfr1onlembfn  6063  tfr1onlemex  6066  tfr1onlemres  6068  tfrcllemsucaccv  6073  tfrcllembfn  6076  tfrcllemex  6079  tfrcllemres  6081  tfrcl  6083  frecabex  6117  frecabcl  6118  frecfcllem  6123  frecrdg  6127  oawordi  6184  nntri3  6212  nnmordi  6227  iserd  6270  relelec  6284  erth  6288  qliftfun  6326  mapsncnv  6404  bren  6416  findcard2d  6559  findcard2sd  6560  isinfinf  6565  tridc  6567  nnwetri  6578  undifdcss  6585  fisseneq  6592  sbthlemi9  6618  supisolem  6647  ordiso2  6672  updjud  6717  elni2  6817  dfplpq2  6857  dfmpq2  6858  enqbreq2  6860  enqdc1  6865  addcmpblnq  6870  addclnq  6878  nqpi  6881  addassnqg  6885  mulassnqg  6887  mulcanenq  6888  distrnqg  6890  1qec  6891  recexnq  6893  subhalfnqq  6917  enq0tr  6937  nqnq0pi  6941  nq0nn  6945  mulcanenq0ec  6948  nnnq0lem1  6949  addclnq0  6954  distrnq0  6962  addassnq0lemcl  6964  elnp1st2nd  6979  prarloc  7006  addlocprlemlt  7034  addlocprlemeq  7036  addlocprlemgt  7037  addclpr  7040  nqprm  7045  mullocprlem  7073  mullocpr  7074  mulclpr  7075  ltpopr  7098  ltaddpr  7100  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemrnd  7108  ltexprlemdisj  7109  addcanprleml  7117  addcanprlemu  7118  addcanprg  7119  recexprlemm  7127  recexprlemopl  7128  recexprlemopu  7130  recexprlemrnd  7132  recexprlemdisj  7133  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemrnd  7153  cauappcvgprlemdisj  7154  cauappcvgprlemlim  7164  caucvgprlemnkj  7169  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemrnd  7176  caucvgprlemlim  7184  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemm  7199  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemrnd  7204  caucvgprprlemexbt  7209  caucvgprprlemlim  7214  prsrlem1  7232  mulclsr  7244  mulasssrg  7248  distrsrg  7249  elreal2  7312  axmulass  7352  axdistr  7353  axcaucvglemcau  7377  add20  7896  mullt0  7902  rereim  8004  ltmul1  8010  cru  8020  mulap0r  8033  divmuldivap  8118  divmuleqap  8123  divadddivap  8133  divmuldivapd  8236  ltmul12a  8256  lemul12a  8258  lemulge11  8262  lediv12a  8290  lediv2a  8291  recgt1i  8294  recreclt  8296  ledivp1  8299  lemul1ad  8335  lemul2ad  8336  ltmul12ad  8337  lemul12ad  8338  lemul12bd  8339  nndivre  8392  nndivtr  8398  halfaddsubcl  8582  halfaddsub  8583  lt2halves  8584  nnrecl  8604  elnn0nn  8648  elnnnn0b  8650  elnnnn0c  8651  nn0addge1  8652  nn0addge2  8653  xnn0xrnemnf  8681  elnn0z  8696  elnnz1  8706  nzadd  8735  elz2  8751  zdivadd  8768  zdivmul  8769  zextle  8770  peano2uz2  8786  uzind  8790  btwnz  8798  uzss  8971  eluzp1m1  8974  eluz2b2  9022  qre  9042  qaddcl  9052  qmulcl  9054  qreccl  9059  irradd  9063  irrmul  9064  cnref1o  9065  rprege0  9080  rprene0  9083  rpreap0  9084  rpcnne0  9085  rpcnap0  9086  rpregt0d  9112  rprege0d  9113  rprene0d  9114  rpcnne0d  9115  lediv2ad  9128  ledivge1le  9135  lediv12ad  9165  nnledivrp  9169  nn0ledivnn  9170  xrlttri3  9199  xrrebnd  9213  xrrege0  9219  elioo4g  9284  ioomax  9298  iccmax  9299  divelunit  9351  elfz5  9364  uzsubsubfz  9393  fzopth  9406  fzass4  9407  fzrev2  9429  uzsplit  9436  elfz2nn0  9456  difelfzle  9473  1fv  9478  4fvwrd4  9479  fzo1fzo0n0  9522  elfzom1elp1fzo  9541  subfzo0  9581  qtri3or  9582  adddivflid  9627  flltdivnn0lt  9639  intfracq  9655  modqid2  9686  modfzo0difsn  9730  iseqvalt  9790  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemab  9822  iseqf1olemmo  9825  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  expclzaplem  9877  leexp1a  9908  expubnd  9910  le2sq2  9928  sumsqeq0  9931  bernneq  9970  expnlbnd  9974  nn0opthd  10026  faclbnd6  10048  facavg  10050  iseqcoll  10143  shftlem  10146  shftfvalg  10148  shftfval  10151  cvg1nlemcau  10312  cvg1nlemres  10313  rexuz3  10318  resqrexlemcvg  10347  resqrexlemglsq  10350  resqrexlemga  10351  sqrtle  10364  sqrtlt  10365  sqrt11  10367  sqrtsq2  10371  absmul  10397  sqabs  10410  abslt  10416  absle  10417  lenegsq  10423  maxleastb  10542  maxltsup  10546  rexanre  10548  negfi  10552  climcn2  10590  mulcn2  10593  isummolem2a  10660  isummo  10662  fisum  10665  dvdsval3  10675  dvdscmul  10698  dvdsmulc  10699  dvdscmulr  10700  dvdsmulcr  10701  modmulconst  10703  dvds2ln  10704  ltoddhalfle  10768  nn0o  10782  divalg2  10801  ndvdssub  10805  ndvdsadd  10806  infssuzex  10820  divgcdz  10838  gcd0id  10845  gcdaddm  10850  bezoutlemstep  10861  bezoutlemmain  10862  dfgcd3  10874  dfgcd2  10878  lcmcllem  10924  dvdslcm  10926  lcmgcdlem  10934  lcmgcdnn  10939  qredeq  10953  qredeu  10954  rpdvds  10956  divgcdcoprm0  10958  cncongr1  10960  cncongr2  10961  cncongrcoprm  10963  prmind2  10977  isprm6  11001  prmexpb  11005  cncongrprm  11011  sqrt2irrlem  11015  pw2dvdslemn  11018  oddpwdclemxy  11022  oddpwdclemdc  11026  oddpwdc  11027  hashdvds  11072  hashgcdlem  11078  bdop  11204  bdunexb  11249  bj-om  11270  findset  11278  bj-peano4  11288  bj-inf2vn  11307  bj-inf2vn2  11308  nninfalllemn  11336  qdencn  11353
  Copyright terms: Public domain W3C validator