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

Theorem simprr 521
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprr ((𝜑 ∧ (𝜓𝜒)) → 𝜒)

Proof of Theorem simprr
StepHypRef Expression
1 id 19 . 2 (𝜒𝜒)
21ad2antll 482 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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simp1rr  1047  simp2rr  1051  simp3rr  1055  disjiun  3924  reg2exmidlema  4449  reg3exmidlemwe  4493  nnsucpred  4530  fvmptt  5512  fcof1  5684  fliftfun  5697  isotr  5717  riotass2  5756  acexmidlemab  5768  ovmpodf  5902  grprinvlem  5965  fnmpoovd  6112  1stconst  6118  2ndconst  6119  cnvf1olem  6121  f1od2  6132  smoiso  6199  tfrcldm  6260  tfrcl  6261  nntr2  6399  swoer  6457  erinxp  6503  ecopovsymg  6528  th3qlem1  6531  f1imaen2g  6687  mapdom1g  6741  fict  6762  fidifsnen  6764  dif1enen  6774  fiunsnnn  6775  fisbth  6777  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fimax2gtri  6795  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  ssfirab  6822  fidcenumlemrk  6842  fidcenumlemr  6843  sbthlemi6  6850  sbthlemi8  6852  isbth  6855  fiuni  6866  supmaxti  6891  infminti  6914  ordiso2  6920  eldju2ndl  6957  eldju2ndr  6958  omp1eomlem  6979  difinfsnlem  6984  difinfinf  6986  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  omniwomnimkv  7039  exmidfodomrlemrALT  7064  acfun  7068  exmidaclem  7069  ccfunen  7084  cc1  7085  cc2lem  7086  dfplpq2  7174  dfmpq2  7175  mulpipqqs  7193  distrnqg  7207  enq0sym  7252  enq0tr  7254  distrnq0  7279  prarloclem3  7317  genplt2i  7330  addlocpr  7356  prmuloc  7386  distrlem1prl  7402  distrlem1pru  7403  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemfl  7429  ltexprlemrl  7430  ltexprlemfu  7431  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  ltaprg  7439  prplnqu  7440  addextpr  7441  recexprlemdisj  7450  recexprlemloc  7451  aptiprleml  7459  aptiprlemu  7460  ltmprr  7462  archpr  7463  cauappcvgprlemopl  7466  cauappcvgprlemopu  7468  cauappcvgprlemdisj  7471  cauappcvgprlemloc  7472  cauappcvgprlem1  7479  cauappcvgprlemlim  7481  caucvgprlemnkj  7486  caucvgprlemopl  7489  caucvgprlemopu  7491  caucvgprlemdisj  7494  caucvgprlemloc  7495  caucvgprprlemnkltj  7509  caucvgprprlemnkeqj  7510  caucvgprprlemnjltk  7511  caucvgprprlemml  7514  caucvgprprlemmu  7515  caucvgprprlemopl  7517  caucvgprprlemopu  7519  caucvgprprlemdisj  7522  caucvgprprlemloc  7523  caucvgprprlemaddq  7528  suplocexprlemrl  7537  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemex  7542  suplocexprlemub  7543  recexgt0sr  7593  mulgt0sr  7598  prsrriota  7608  suplocsrlem  7628  addcnsr  7654  mulcnsr  7655  mulcnsrec  7663  axmulcom  7691  rereceu  7709  axarch  7711  axcaucvglemres  7719  axpre-suploclemres  7721  lelttr  7864  ltletr  7865  addcan  7954  addcan2  7955  addsub4  8017  ltadd2  8193  le2add  8218  lt2add  8219  lt2sub  8234  le2sub  8235  eqord1  8257  rereim  8360  apreap  8361  apreim  8377  mulreim  8378  apcotr  8381  apadd1  8382  addext  8384  apneg  8385  mulext1  8386  mulext  8388  ltleap  8406  aprcl  8420  mulap0  8427  mulcanapd  8434  rec11ap  8482  rec11rap  8483  divdivdivap  8485  ddcanap  8498  divadddivap  8499  prodgt0gt0  8621  prodgt0  8622  prodge0  8624  lemulge11  8636  lt2mul2div  8649  ltrec  8653  lerec  8654  lerec2  8659  ledivp1  8673  mulle0r  8714  nn0ge0div  9150  suprzclex  9161  qapne  9443  xrlelttr  9601  xrltletr  9602  xrre3  9617  xrrege0  9620  xaddge0  9673  xle2add  9674  xlt2add  9675  fzass4  9854  fzrev  9876  elfz1b  9882  eluzgtdifelfzo  9986  fzocatel  9988  exbtwnzlemex  10039  rebtwn2z  10044  modqid  10134  modqcyc  10144  modqaddabs  10147  modqaddmod  10148  mulqaddmodid  10149  modqadd2mod  10159  modqltm1p1mod  10161  modqsubmod  10167  modqsubmodmod  10168  modaddmodup  10172  modqmulmod  10174  modqmulmodr  10175  modqaddmulmod  10176  modqsubdir  10178  frec2uzisod  10192  uzennn  10221  iseqovex  10241  seqvalcd  10244  seqf  10246  seqovcd  10248  seq3shft2  10258  monoord  10261  iseqf1olemnab  10273  seq3distr  10298  expnegzap  10339  ltexp2a  10357  le2sq2  10380  bernneq  10424  expnlbnd2  10429  nn0opth2  10482  faclbnd  10499  bcval5  10521  hashcl  10539  hashen  10542  fihashdom  10561  hashunlem  10562  hashun  10563  hashxp  10584  fimaxq  10585  zfz1isolem1  10595  zfz1iso  10596  seq3coll  10597  cvg1nlemres  10769  cvg1n  10770  resqrexlemp1rp  10790  resqrexlemoverl  10805  resqrexlemex  10809  sqrtsq  10828  abslt  10872  absle  10873  abs3lem  10895  maxleastlt  10999  maxltsup  11002  fimaxre2  11010  negfi  11011  xrmaxleastlt  11037  xrmaxltsup  11039  xrmaxaddlem  11041  2clim  11082  climcn2  11090  addcn2  11091  mulcn2  11093  reccn2ap  11094  climge0  11106  climcau  11128  summodclem2  11163  summodc  11164  zsumdc  11165  fsumf1o  11171  fisumss  11173  fsum3cvg3  11177  fsumcl2lem  11179  fsumadd  11187  mptfzshft  11223  fsumrev  11224  fsummulc2  11229  fsumconst  11235  modfsummod  11239  fsumrelem  11252  binom  11265  cvgratnn  11312  mertenslemub  11315  prodmodclem2  11358  prodmodc  11359  efcllem  11377  tanaddaplem  11456  moddvds  11513  dvdsflip  11560  oexpneg  11585  nn0o  11615  fldivndvdslt  11643  zsupcllemstep  11649  zsupcllemex  11650  zssinfcl  11652  bezoutlemnewy  11695  bezoutlemstep  11696  bezoutlemeu  11706  dfgcd3  11709  dfgcd2  11713  dvdsmulgcd  11724  bezoutr  11731  lcmgcdlem  11769  coprmdvds2  11785  qredeu  11789  rpdvds  11791  cncongr1  11795  prmind2  11812  isprm6  11836  oddpwdclemdc  11862  nonsq  11896  hashdvds  11908  crth  11911  hashgcdlem  11914  hashgcdeq  11915  ennnfonelemg  11927  ennnfonelemex  11938  ennnfonelemrnh  11940  ennnfonelemf1  11942  ennnfonelemrn  11943  ennnfonelemdm  11944  ennnfonelemim  11948  ennnfone  11949  ctinf  11954  ctiunctlemfo  11963  isstruct2r  11984  setscom  12013  iuncld  12298  ssnei2  12340  topssnei  12345  restopnb  12364  cnfval  12377  cnpfval  12378  iscnp4  12401  cnptopco  12405  cncnpi  12411  cncnp  12413  cnconst2  12416  cnrest2  12419  cnptoprest  12422  cnptoprest2  12423  cnpdis  12425  lmss  12429  lmtopcnp  12433  neitx  12451  txcnp  12454  txrest  12459  txdis1cn  12461  txlm  12462  cnmpt21  12474  imasnopn  12482  xmetres2  12562  blvalps  12571  blval  12572  elbl2ps  12575  elbl2  12576  blhalf  12591  blssexps  12612  blssex  12613  ssblex  12614  blin2  12615  bdmetval  12683  xmetxp  12690  xmettx  12693  metcnpi3  12700  txmetcnp  12701  addcncntoplem  12734  fsumcncntop  12739  elcncf2  12744  mulc1cncf  12759  cncfco  12761  cncfmet  12762  cncfmptc  12765  mulcncf  12774  dedekindeulemub  12779  dedekindeulemloc  12780  dedekindeulemlu  12782  dedekindeu  12784  dedekindicclemub  12788  dedekindicclemloc  12789  dedekindicclemlu  12791  dedekindicclemicc  12793  dedekindicc  12794  ivthinclemlopn  12797  ivthinclemuopn  12799  limcimo  12817  cnplimccntop  12822  limccnp2lem  12828  limccnp2cntop  12829  dvfvalap  12833  dveflem  12870  reeff1olem  12875  reeff1oleme  12876  eflt  12879  sin0pilem2  12885  pilem3  12886  ioocosf1o  12957  nnti  13250  pwtrufal  13251  pwf1oexmid  13253  sssneq  13256  qdencn  13283  cvgcmp2n  13289  trilpolemlt1  13295  trirec0  13298  supfz  13303  inffz  13304
  Copyright terms: Public domain W3C validator