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

Theorem simprl 491
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 467 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  simp1rl  980  simp2rl  984  simp3rl  988  rmob  2878  reg3exmidlemwe  4331  0xp  4448  imainss  4767  fvmptt  5290  fcof1o  5457  isotr  5484  riota5f  5520  ovmpt2df  5660  grprinvlem  5723  grpridd  5725  unielxp  5828  1stconst  5870  2ndconst  5871  cnvf1olem  5873  tfrlemi14d  5978  tfrexlem  5979  nnaordi  6112  swoer  6165  qliftfun  6219  ecopovsymg  6236  th3qlem1  6239  fidifsnen  6362  fisbth  6371  findcard2d  6379  findcard2sd  6380  diffisn  6381  diffifi  6382  ac6sfi  6383  fientri3  6384  nnwetri  6385  ordiso2  6415  dfplpq2  6510  dfmpq2  6511  mulpipqqs  6529  distrnqg  6543  ltexnqq  6564  subhalfnqq  6570  distrnq0  6615  prarloclemup  6651  prarloclem3  6653  prarloc  6659  genplt2i  6666  nqprl  6707  nqpru  6708  prmuloc  6722  mullocpr  6727  distrlem4prl  6740  distrlem4pru  6741  ltaddpr  6753  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemrl  6766  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  ltaprlem  6774  ltaprg  6775  prplnqu  6776  addextpr  6777  recexprlemdisj  6786  recexprlemloc  6787  recexprlem1ssl  6789  aptiprleml  6795  aptiprlemu  6796  ltmprr  6798  archpr  6799  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlem1  6815  cauappcvgprlem2  6816  cauappcvgprlemlim  6817  caucvgprlemnkj  6822  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlem2  6836  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemopu  6855  caucvgprprlemdisj  6858  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemaddq  6864  caucvgprprlem2  6866  recexgt0sr  6916  mulgt0sr  6920  prsrriota  6930  caucvgsrlemoffres  6942  addcnsr  6968  mulcnsr  6969  mulcnsrec  6977  axaddcl  6998  axmulcl  7000  axmulcom  7003  rereceu  7021  recriota  7022  axcaucvglemres  7031  lelttr  7165  ltletr  7166  readdcan  7214  addcan  7254  addcan2  7255  addsub4  7317  ltadd2  7488  le2add  7513  lt2add  7514  lt2sub  7529  le2sub  7530  rimul  7650  rereim  7651  ltmul1  7657  apreim  7668  mulreim  7669  apcotr  7672  apadd1  7673  addext  7675  apneg  7676  mulext1  7677  mulext  7679  ltleap  7695  mulap0  7709  mulcanapd  7716  receuap  7724  rec11ap  7761  rec11rap  7762  divdivdivap  7764  ddcanap  7777  divadddivap  7778  conjmulap  7780  prodgt0gt0  7892  prodge0  7895  ltmul12a  7901  lemulge11  7907  lt2mul2div  7920  ltrec  7924  lerec  7925  lt2msq  7927  lerec2  7930  le2msq  7942  msq11  7943  ledivp1  7944  mulle0r  7985  peano5uzti  8405  qapne  8671  xrlelttr  8823  xrltletr  8824  xrre  8834  divelunit  8971  fzass4  9027  fzocatel  9157  qbtwnzlemex  9207  rebtwn2z  9211  qbtwnre  9213  modqid  9299  modqcyc  9309  modqaddabs  9312  modqaddmod  9313  mulqaddmodid  9314  modqadd2mod  9324  modqltm1p1mod  9326  modqsubmod  9332  modqsubmodmod  9333  modqmulmod  9339  modqmulmodr  9340  modqaddmulmod  9341  modqsubdir  9343  frec2uzisod  9357  iseqovex  9383  iseqval  9384  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  iseqdistr  9414  expivallem  9421  expcl2lemap  9432  expnegzap  9454  ltexp2a  9472  le2sq2  9495  nn0opth2  9592  ibcval5  9631  cvg1nlemres  9812  cvg1n  9813  recvguniq  9822  resqrexlemp1rp  9833  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemex  9852  sqrtmul  9862  sqrtsq  9871  absexpzap  9907  absle  9916  abs3lem  9938  amgm2  9945  climcn2  10061  addcn2  10062  mulcn2  10064  climcau  10097  dvdsval2  10111  moddvds  10117  dvdsabseq  10159  dvdsflip  10163  oexpneg  10188  fldivndvdslt  10247  pw2dvdslemn  10253  ialgrlem1st  10264  qdencn  10511
  Copyright terms: Public domain W3C validator