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

Theorem simprr 484
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 460 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  simp1rr  970  simp2rr  974  simp3rr  978  reg2exmidlema  4259  reg3exmidlemwe  4303  fvmptt  5262  fcof1  5423  fliftfun  5436  isotr  5456  riotass2  5494  acexmidlemab  5506  ovmpt2df  5632  grprinvlem  5695  1stconst  5842  2ndconst  5843  cnvf1olem  5845  smoiso  5917  swoer  6134  erinxp  6180  ecopovsymg  6205  th3qlem1  6208  f1imaen2g  6273  fidifsnen  6331  fiunsnnn  6338  fisbth  6340  findcard2d  6348  findcard2sd  6349  diffifi  6351  ac6sfi  6352  nnwetri  6354  ordiso2  6355  dfplpq2  6450  dfmpq2  6451  mulpipqqs  6469  distrnqg  6483  enq0sym  6528  enq0tr  6530  distrnq0  6555  prarloclem3  6593  genplt2i  6606  addlocpr  6632  prmuloc  6662  distrlem1prl  6678  distrlem1pru  6679  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  addcanprleml  6710  addcanprlemu  6711  ltaprg  6715  prplnqu  6716  addextpr  6717  recexprlemdisj  6726  recexprlemloc  6727  aptiprleml  6735  aptiprlemu  6736  ltmprr  6738  archpr  6739  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlem1  6755  cauappcvgprlemlim  6757  caucvgprlemnkj  6762  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemdisj  6798  caucvgprprlemloc  6799  caucvgprprlemaddq  6804  recexgt0sr  6856  mulgt0sr  6860  prsrriota  6870  addcnsr  6908  mulcnsr  6909  mulcnsrec  6917  axmulcom  6943  rereceu  6961  axarch  6963  axcaucvglemres  6971  lelttr  7104  ltletr  7105  addcan  7189  addcan2  7190  addsub4  7252  ltadd2  7414  le2add  7437  lt2add  7438  lt2sub  7453  le2sub  7454  rereim  7575  apreap  7576  apreim  7592  mulreim  7593  apcotr  7596  apadd1  7597  addext  7599  apneg  7600  mulext1  7601  mulext  7603  ltleap  7619  mulap0  7633  mulcanapd  7640  rec11ap  7684  rec11rap  7685  divdivdivap  7687  ddcanap  7700  divadddivap  7701  prodgt0gt0  7815  prodgt0  7816  prodge0  7818  lemulge11  7830  lt2mul2div  7843  ltrec  7847  lerec  7848  lerec2  7853  ledivp1  7867  nn0ge0div  8325  qapne  8572  xrlelttr  8720  xrltletr  8721  xrre3  8733  xrrege0  8736  fzass4  8923  fzrev  8944  elfz1b  8950  eluzgtdifelfzo  9051  fzocatel  9053  qbtwnzlemex  9103  rebtwn2z  9107  frec2uzisod  9167  iseqovex  9193  iseqval  9194  iseqshft2  9206  monoord  9209  iseqdistr  9223  expnegzap  9263  ltexp2a  9280  le2sq2  9303  bernneq  9343  expnlbnd2  9348  cvg1nlemres  9558  cvg1n  9559  resqrexlemp1rp  9578  resqrexlemoverl  9593  resqrexlemex  9597  sqrtsq  9616  abslt  9658  absle  9659  abs3lem  9681  2clim  9796  climcn2  9804  addcn2  9805  mulcn2  9807  climge0  9819  climcau  9840
  Copyright terms: Public domain W3C validator