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

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

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
21ad2antrl 459 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:  simp1rl  969  simp2rl  973  simp3rl  977  rmob  2850  reg3exmidlemwe  4303  0xp  4420  imainss  4739  fvmptt  5262  fcof1o  5429  isotr  5456  riota5f  5492  ovmpt2df  5632  grprinvlem  5695  grpridd  5697  unielxp  5800  1stconst  5842  2ndconst  5843  cnvf1olem  5845  tfrlemi14d  5947  tfrexlem  5948  nnaordi  6081  swoer  6134  qliftfun  6188  ecopovsymg  6205  th3qlem1  6208  fidifsnen  6331  fisbth  6340  findcard2d  6348  findcard2sd  6349  diffisn  6350  diffifi  6351  ac6sfi  6352  fientri3  6353  nnwetri  6354  ordiso2  6355  dfplpq2  6450  dfmpq2  6451  mulpipqqs  6469  distrnqg  6483  ltexnqq  6504  subhalfnqq  6510  distrnq0  6555  prarloclemup  6591  prarloclem3  6593  prarloc  6599  genplt2i  6606  nqprl  6647  nqpru  6648  prmuloc  6662  mullocpr  6667  distrlem4prl  6680  distrlem4pru  6681  ltaddpr  6693  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemrl  6706  ltexprlemru  6708  addcanprleml  6710  addcanprlemu  6711  ltaprlem  6714  ltaprg  6715  prplnqu  6716  addextpr  6717  recexprlemdisj  6726  recexprlemloc  6727  recexprlem1ssl  6729  aptiprleml  6735  aptiprlemu  6736  ltmprr  6738  archpr  6739  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlem1  6755  cauappcvgprlem2  6756  cauappcvgprlemlim  6757  caucvgprlemnkj  6762  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlem2  6776  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemdisj  6798  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemaddq  6804  caucvgprprlem2  6806  recexgt0sr  6856  mulgt0sr  6860  prsrriota  6870  caucvgsrlemoffres  6882  addcnsr  6908  mulcnsr  6909  mulcnsrec  6917  axaddcl  6938  axmulcl  6940  axmulcom  6943  rereceu  6961  recriota  6962  axcaucvglemres  6971  lelttr  7104  ltletr  7105  readdcan  7151  addcan  7189  addcan2  7190  addsub4  7252  ltadd2  7414  le2add  7437  lt2add  7438  lt2sub  7453  le2sub  7454  rimul  7574  rereim  7575  ltmul1  7581  apreim  7592  mulreim  7593  apcotr  7596  apadd1  7597  addext  7599  apneg  7600  mulext1  7601  mulext  7603  ltleap  7619  mulap0  7633  mulcanapd  7640  receuap  7648  rec11ap  7684  rec11rap  7685  divdivdivap  7687  ddcanap  7700  divadddivap  7701  conjmulap  7703  prodgt0gt0  7815  prodge0  7818  ltmul12a  7824  lemulge11  7830  lt2mul2div  7843  ltrec  7847  lerec  7848  lt2msq  7850  lerec2  7853  le2msq  7865  msq11  7866  ledivp1  7867  peano5uzti  8344  qapne  8572  xrlelttr  8720  xrltletr  8721  xrre  8731  divelunit  8868  fzass4  8923  fzocatel  9053  qbtwnzlemex  9103  rebtwn2z  9107  qbtwnre  9109  frec2uzisod  9167  iseqovex  9193  iseqval  9194  iseqfveq2  9202  iseqshft2  9206  monoord  9209  iseqsplit  9212  iseqdistr  9223  expivallem  9230  expcl2lemap  9241  expnegzap  9263  ltexp2a  9280  le2sq2  9303  cvg1nlemres  9558  cvg1n  9559  recvguniq  9567  resqrexlemp1rp  9578  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemex  9597  sqrtmul  9607  sqrtsq  9616  absexpzap  9650  absle  9659  abs3lem  9681  amgm2  9688  climcn2  9804  addcn2  9805  mulcn2  9807  climcau  9840  ialgrlem1st  9855
  Copyright terms: Public domain W3C validator