ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jca GIF 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 (𝜑𝜓)
jca.2 (𝜑𝜒)
Assertion
Ref Expression
jca (𝜑 → (𝜓𝜒))

Proof of Theorem jca
StepHypRef Expression
1 jca.1 . 2 (𝜑𝜓)
2 jca.2 . 2 (𝜑𝜒)
3 pm3.2 138 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 62 1 (𝜑 → (𝜓𝜒))
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  8315  ltmul1  8321  cru  8331  mulap0r  8344  aprcl  8375  divmuldivap  8439  divmuleqap  8444  divadddivap  8454  divmuldivapd  8559  div2subap  8563  ltmul12a  8582  lemul12a  8584  lemulge11  8588  lediv12a  8616  lediv2a  8617  recgt1i  8620  recreclt  8622  ledivp1  8625  lemul1ad  8661  lemul2ad  8662  ltmul12ad  8663  lemul12ad  8664  lemul12bd  8665  nndivre  8720  nndivtr  8726  halfaddsubcl  8911  halfaddsub  8912  lt2halves  8913  nnrecl  8933  elnn0nn  8977  elnnnn0b  8979  elnnnn0c  8980  nn0addge1  8981  nn0addge2  8982  xnn0xrnemnf  9010  elnn0z  9025  elnnz1  9035  nzadd  9064  elz2  9080  zdivadd  9098  zdivmul  9099  zextle  9100  peano2uz2  9116  uzind  9120  btwnz  9128  uzss  9302  eluzp1m1  9305  eluz2b2  9353  qre  9373  qaddcl  9383  qmulcl  9385  qreccl  9390  irradd  9394  irrmul  9395  cnref1o  9396  rprege0  9411  rprene0  9414  rpreap0  9415  rpcnne0  9416  rpcnap0  9417  rpregt0d  9445  rprege0d  9446  rprene0d  9447  rpcnne0d  9448  lediv2ad  9461  ledivge1le  9468  lediv12ad  9498  nnledivrp  9508  nn0ledivnn  9509  xrlttri3  9538  xrrebnd  9557  xrrege0  9563  xnn0xadd0  9605  xlesubadd  9621  elioo4g  9672  ioomax  9686  iccmax  9687  divelunit  9740  elfz5  9753  uzsubsubfz  9782  fzopth  9796  fzass4  9797  fzrev2  9820  uzsplit  9827  elfz2nn0  9847  difelfzle  9866  1fv  9871  4fvwrd4  9872  fzo1fzo0n0  9915  elfzom1elp1fzo  9934  subfzo0  9974  qtri3or  9975  adddivflid  10020  flltdivnn0lt  10032  intfracq  10048  modqid2  10079  modfzo0difsn  10123  seq3val  10186  seqvalcd  10187  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemmo  10220  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  expclzaplem  10272  leexp1a  10303  expubnd  10305  le2sq2  10323  sumsqeq0  10326  bernneq  10367  expnlbnd  10371  nn0opthd  10423  faclbnd6  10445  facavg  10447  seq3coll  10540  shftlem  10543  shftfvalg  10545  shftfval  10548  cvg1nlemcau  10711  cvg1nlemres  10712  rexuz3  10717  resqrexlemcvg  10746  resqrexlemglsq  10749  resqrexlemga  10750  sqrtle  10763  sqrtlt  10764  sqrt11  10766  sqrtsq2  10770  absmul  10796  sqabs  10809  abslt  10815  absle  10816  lenegsq  10822  maxleastb  10941  maxltsup  10945  rexanre  10947  negfi  10954  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxltsup  10982  xrmaxadd  10985  climcn2  11033  mulcn2  11036  summodclem2a  11105  summodc  11107  fsum3  11111  fsum3cvg3  11120  fsumcl2lem  11122  fsumadd  11130  fsump1i  11157  fsum0diaglem  11164  mptfzshft  11166  fsumrev  11167  fsummulc2  11172  fsum00  11186  expcnvap0  11226  mertenslemi1  11259  eftlub  11310  efieq  11356  sincos1sgn  11385  demoivreALT  11394  dvdsval3  11409  dvdscmul  11432  dvdsmulc  11433  dvdscmulr  11434  dvdsmulcr  11435  modmulconst  11437  dvds2ln  11438  ltoddhalfle  11502  nn0o  11516  divalg2  11535  ndvdssub  11539  ndvdsadd  11540  infssuzex  11554  divgcdz  11572  gcd0id  11579  gcdaddm  11584  bezoutlemstep  11597  bezoutlemmain  11598  dfgcd3  11610  dfgcd2  11614  lcmcllem  11660  dvdslcm  11662  lcmgcdlem  11670  lcmgcdnn  11675  qredeq  11689  qredeu  11690  rpdvds  11692  divgcdcoprm0  11694  cncongr1  11696  cncongr2  11697  cncongrcoprm  11699  prmind2  11713  isprm6  11737  prmexpb  11741  cncongrprm  11747  sqrt2irrlem  11751  pw2dvdslemn  11754  oddpwdclemxy  11758  oddpwdclemdc  11762  oddpwdc  11763  hashdvds  11808  hashgcdlem  11814  ennnfonelemfun  11841  ennnfonelemim  11848  ctinfomlemom  11851  ctinfom  11852  ctinf  11854  ctiunctlemfo  11863  topgele  12107  tgcl  12144  epttop  12170  opnssneib  12236  iscnp4  12298  cnco  12301  cncnp  12310  cnrest2  12316  lmss  12326  txcnp  12351  txcn  12355  cnmpt12  12367  cnmpt22  12374  hmeof1o  12389  psmetres2  12413  distspace  12415  ismeti  12426  isxmetd  12427  xmetpsmet  12449  xblss2ps  12484  xblss2  12485  blcntrps  12495  blcntr  12496  blin2  12512  mopni3  12564  metequiv2  12576  bdmet  12582  xmettx  12590  cnbl0  12614  cnblcld  12615  tgioo  12626  elcncf1di  12646  dedekindeulemlu  12679  suplociccex  12683  dedekindicclemlu  12688  dedekindicc  12691  ivthinclemlopn  12694  ivthdec  12702  cnplimcim  12716  limccnp2lem  12725  dvfvalap  12730  sin0pilem1  12773  pilem3  12775  ptolemy  12816  sincosq1sgn  12818  sinq12gt0  12822  bj-nnan  12844  bdop  12969  bdunexb  13014  bj-om  13031  findset  13039  bj-peano4  13049  bj-inf2vn  13068  bj-inf2vn2  13069  pwle2  13089  pwf1oexmid  13090  nninfalllemn  13098  sbthom  13117  qdencn  13118  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator