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  414  jcab  593  ioran  742  ordi  806  stdcndc  831  stdcndcOLD  832  dfandc  870  pm4.55dc  923  mpbi2and  928  mpbir2and  929  pm4.82  935  pm4.83dc  936  rnlem  961  syl22anc  1218  syl112anc  1221  syl121anc  1222  syl211anc  1223  syl23anc  1224  syl32anc  1225  syl122anc  1226  syl212anc  1227  syl221anc  1228  syl222anc  1233  syl123anc  1234  syl132anc  1235  syl213anc  1236  syl231anc  1237  syl312anc  1238  syl321anc  1239  syl223anc  1243  syl232anc  1244  syl322anc  1245  syl233anc  1246  syl323anc  1247  syl332anc  1248  ecased  1328  19.26  1458  nfand  1548  19.40  1611  equsexd  1708  sbcof2  1783  sbequ8  1820  eu2  2044  eu3h  2045  eu5  2047  mooran2  2073  datisi  2110  felapton  2114  darapti  2115  dimatis  2117  fresison  2118  fesapo  2120  reximssdv  2539  r19.26  2561  r19.29af2  2575  r19.40  2588  eqvinc  2812  eqvincg  2813  elrabd  2846  reu6  2877  reu3  2878  indifdir  3337  undif3ss  3342  un00  3414  eqifdc  3511  disjpr2  3595  prel12  3706  prneimg  3709  preqsn  3710  disjiun  3932  opth  4167  0nelop  4178  euotd  4184  opelopabsb  4190  ispod  4234  elon2  4306  unexb  4371  opeluu  4379  eusvnfb  4383  suc11g  4480  nlimsucg  4489  tfi  4504  vtoclr  4595  opthprc  4598  ideqg  4698  resiexg  4872  dminss  4961  imainss  4962  ssxpbm  4982  relrelss  5073  funopg  5165  fntpg  5187  fun11uni  5201  imain  5213  funimaexglem  5214  funssxp  5300  ffdm  5301  f00  5322  dffo2  5357  fodmrnu  5361  foco  5363  fun11iun  5396  f1o00  5410  fsnd  5418  fv3  5452  dff2  5572  dff3im  5573  dffo4  5576  ffnfv  5586  ffvresb  5591  fsn2  5602  fconstfvm  5646  fnfvima  5660  fcof1o  5698  isocnv  5720  isotr  5725  riotaprop  5761  acexmidlemcase  5777  caovlem2d  5971  f1ocnvd  5980  caofcom  6013  resfunexgALT  6016  elxp7  6076  2ndrn  6089  1stconst  6126  2ndconst  6127  cnvf1olem  6129  poxp  6137  dftpos4  6168  dfsmo2  6192  tfrlem5  6219  tfrlemiex  6236  tfr1onlemsucaccv  6246  tfr1onlembfn  6249  tfr1onlemex  6252  tfr1onlemres  6254  tfrcllemsucaccv  6259  tfrcllembfn  6262  tfrcllemex  6265  tfrcllemres  6267  tfrcl  6269  frecabex  6303  frecabcl  6304  frecfcllem  6309  frecrdg  6313  oawordi  6373  nntri3  6401  nntr2  6407  nnmordi  6420  iserd  6463  relelec  6477  erth  6481  qliftfun  6519  mapsncnv  6597  mptelixpg  6636  bren  6649  findcard2d  6793  findcard2sd  6794  isinfinf  6799  tridc  6801  nnwetri  6812  undifdcss  6819  fiintim  6825  fisseneq  6828  fidcenumlemim  6848  sbthlemi9  6861  supisolem  6903  ordiso2  6928  updjud  6975  difinfsn  6993  ctssdccl  7004  omniwomnimkv  7049  acfun  7080  ccfunen  7096  cc4f  7101  cc4n  7103  elni2  7146  dfplpq2  7186  dfmpq2  7187  enqbreq2  7189  enqdc1  7194  addcmpblnq  7199  addclnq  7207  nqpi  7210  addassnqg  7214  mulassnqg  7216  mulcanenq  7217  distrnqg  7219  1qec  7220  recexnq  7222  subhalfnqq  7246  enq0tr  7266  nqnq0pi  7270  nq0nn  7274  mulcanenq0ec  7277  nnnq0lem1  7278  addclnq0  7283  distrnq0  7291  addassnq0lemcl  7293  elnp1st2nd  7308  prarloc  7335  addlocprlemlt  7363  addlocprlemeq  7365  addlocprlemgt  7366  addclpr  7369  nqprm  7374  mullocprlem  7402  mullocpr  7403  mulclpr  7404  ltpopr  7427  ltaddpr  7429  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemrnd  7437  ltexprlemdisj  7438  addcanprleml  7446  addcanprlemu  7447  addcanprg  7448  recexprlemm  7456  recexprlemopl  7457  recexprlemopu  7459  recexprlemrnd  7461  recexprlemdisj  7462  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemrnd  7482  cauappcvgprlemdisj  7483  cauappcvgprlemlim  7493  caucvgprlemnkj  7498  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemrnd  7505  caucvgprlemlim  7513  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemm  7528  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemrnd  7533  caucvgprprlemexbt  7538  caucvgprprlemlim  7543  suplocexprlemrl  7549  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemub  7555  prsrlem1  7574  mulclsr  7586  mulasssrg  7590  distrsrg  7591  suplocsrlemb  7638  elreal2  7662  axmulass  7705  axdistr  7706  axcaucvglemcau  7730  add20  8260  mullt0  8266  rereim  8372  ltmul1  8378  cru  8388  mulap0r  8401  aprcl  8432  divmuldivap  8496  divmuleqap  8501  divadddivap  8511  divmuldivapd  8616  div2subap  8620  ltmul12a  8642  lemul12a  8644  lemulge11  8648  lediv12a  8676  lediv2a  8677  recgt1i  8680  recreclt  8682  ledivp1  8685  lemul1ad  8721  lemul2ad  8722  ltmul12ad  8723  lemul12ad  8724  lemul12bd  8725  nndivre  8780  nndivtr  8786  halfaddsubcl  8977  halfaddsub  8978  lt2halves  8979  nnrecl  8999  elnn0nn  9043  elnnnn0b  9045  elnnnn0c  9046  nn0addge1  9047  nn0addge2  9048  xnn0xrnemnf  9076  elnn0z  9091  elnnz1  9101  nzadd  9130  elz2  9146  zdivadd  9164  zdivmul  9165  zextle  9166  peano2uz2  9182  uzind  9186  btwnz  9194  uzss  9370  eluzp1m1  9373  eluz2b2  9424  qre  9444  qaddcl  9454  qmulcl  9456  qreccl  9461  irradd  9465  irrmul  9466  elpqb  9468  cnref1o  9469  rprege0  9485  rprene0  9488  rpreap0  9489  rpcnne0  9490  rpcnap0  9491  rpregt0d  9520  rprege0d  9521  rprene0d  9522  rpcnne0d  9523  lediv2ad  9536  ledivge1le  9543  lediv12ad  9573  nnledivrp  9583  nn0ledivnn  9584  xrlttri3  9613  xrrebnd  9632  xrrege0  9638  xnn0xadd0  9680  xlesubadd  9696  elioo4g  9747  ioomax  9761  iccmax  9762  divelunit  9815  elfz5  9829  uzsubsubfz  9858  fzopth  9872  fzass4  9873  fzrev2  9896  uzsplit  9903  elfz2nn0  9923  difelfzle  9942  1fv  9947  4fvwrd4  9948  fzo1fzo0n0  9991  elfzom1elp1fzo  10010  subfzo0  10050  qtri3or  10051  adddivflid  10096  flltdivnn0lt  10108  intfracq  10124  modqid2  10155  modfzo0difsn  10199  seq3val  10262  seqvalcd  10263  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemmo  10296  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  expclzaplem  10348  leexp1a  10379  expubnd  10381  le2sq2  10399  sumsqeq0  10402  bernneq  10443  expnlbnd  10447  nn0opthd  10500  faclbnd6  10522  facavg  10524  seq3coll  10617  shftlem  10620  shftfvalg  10622  shftfval  10625  cvg1nlemcau  10788  cvg1nlemres  10789  rexuz3  10794  resqrexlemcvg  10823  resqrexlemglsq  10826  resqrexlemga  10827  sqrtle  10840  sqrtlt  10841  sqrt11  10843  sqrtsq2  10847  absmul  10873  sqabs  10886  abslt  10892  absle  10893  lenegsq  10899  maxleastb  11018  maxltsup  11022  rexanre  11024  negfi  11031  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxltsup  11059  xrmaxadd  11062  climcn2  11110  mulcn2  11113  summodclem2a  11182  summodc  11184  fsum3  11188  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  fsump1i  11234  fsum0diaglem  11241  mptfzshft  11243  fsumrev  11244  fsummulc2  11249  fsum00  11263  expcnvap0  11303  mertenslemi1  11336  ntrivcvgap0  11350  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  eftlub  11433  efieq  11478  sincos1sgn  11507  demoivreALT  11516  dvdsval3  11533  dvdscmul  11556  dvdsmulc  11557  dvdscmulr  11558  dvdsmulcr  11559  modmulconst  11561  dvds2ln  11562  ltoddhalfle  11626  nn0o  11640  divalg2  11659  ndvdssub  11663  ndvdsadd  11664  infssuzex  11678  divgcdz  11696  gcd0id  11703  gcdaddm  11708  bezoutlemstep  11721  bezoutlemmain  11722  dfgcd3  11734  dfgcd2  11738  lcmcllem  11784  dvdslcm  11786  lcmgcdlem  11794  lcmgcdnn  11799  qredeq  11813  qredeu  11814  rpdvds  11816  divgcdcoprm0  11818  cncongr1  11820  cncongr2  11821  cncongrcoprm  11823  prmind2  11837  isprm6  11861  prmexpb  11865  cncongrprm  11871  sqrt2irrlem  11875  pw2dvdslemn  11879  oddpwdclemxy  11883  oddpwdclemdc  11887  oddpwdc  11888  hashdvds  11933  hashgcdlem  11939  ennnfonelemfun  11966  ennnfonelemim  11973  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  ctiunctlemfo  11988  omctfn  11992  topgele  12235  tgcl  12272  epttop  12298  opnssneib  12364  iscnp4  12426  cnco  12429  cncnp  12438  cnrest2  12444  lmss  12454  txcnp  12479  txcn  12483  cnmpt12  12495  cnmpt22  12502  hmeof1o  12517  psmetres2  12541  distspace  12543  ismeti  12554  isxmetd  12555  xmetpsmet  12577  xblss2ps  12612  xblss2  12613  blcntrps  12623  blcntr  12624  blin2  12640  mopni3  12692  metequiv2  12704  bdmet  12710  xmettx  12718  cnbl0  12742  cnblcld  12743  tgioo  12754  elcncf1di  12774  dedekindeulemlu  12807  suplociccex  12811  dedekindicclemlu  12816  dedekindicc  12819  ivthinclemlopn  12822  ivthdec  12830  cnplimcim  12844  limccnp2lem  12853  dvfvalap  12858  reeff1olem  12900  sin0pilem1  12910  pilem3  12912  ptolemy  12953  sincosq1sgn  12955  sinq12gt0  12959  ioocosf1o  12983  rprelogbmulexp  13081  bj-nnan  13119  bdop  13244  bdunexb  13289  bj-om  13306  findset  13314  bj-peano4  13324  bj-inf2vn  13343  bj-inf2vn2  13344  pwle2  13366  pwf1oexmid  13367  nninfalllemn  13377  sbthom  13396  qdencn  13397  trilpolemlt1  13409
  Copyright terms: Public domain W3C validator