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

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

Proof of Theorem simpll
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
21ad2antrr 457 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:  simp1ll  967  simp2ll  971  simp3ll  975  rmob  2850  prneimg  3545  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  poinxp  4409  mpteqb  5261  fvmptt  5262  fcof1  5423  acexmid  5511  grprinvlem  5695  dftpos4  5878  tfrlem3ag  5924  tfrlem3a  5925  tfrlemi1  5946  tfrexlem  5948  nndifsnid  6080  qsel  6183  ecopovsymg  6205  ecopoverg  6207  th3qlem1  6208  fidifsnid  6332  findcard2  6346  findcard2s  6347  findcard2sd  6349  dfplpq2  6450  dfmpq2  6451  mulpipqqs  6469  distrnqg  6483  ltexnqq  6504  subhalfnqq  6510  prarloclemarch  6514  nnnq0lem1  6542  distrnq0  6555  npsspw  6567  prarloclemlo  6590  prarloclem3  6593  prarloclemcalc  6598  genplt2i  6606  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  ltprordil  6685  ltexprlemlol  6698  ltexprlemupu  6700  addextpr  6717  recexprlemopl  6721  recexprlemdisj  6726  recexprlem1ssl  6729  aptiprleml  6735  prsrlem1  6825  recexgt0sr  6856  addcnsr  6908  mulcnsr  6909  mulcnsrec  6917  axaddcl  6938  axmulcl  6940  axmulcom  6943  rereceu  6961  cnegexlem1  7184  cnegex  7187  addsub4  7252  le2add  7437  lt2add  7438  lt2sub  7453  le2sub  7454  rereim  7575  apreim  7592  mulreim  7593  addext  7599  mulext  7603  receuap  7648  rec11ap  7684  rec11rap  7685  divdivdivap  7687  ddcanap  7700  divadddivap  7701  divsubdivap  7702  conjmulap  7703  rerecclap  7704  recgt0  7814  prodgt0gt0  7815  prodgt0  7816  prodge0  7818  ltmul12a  7824  lemul12a  7826  lemulge11  7830  lt2mul2div  7843  ltrec  7847  lerec  7848  lt2msq  7850  ltrec1  7852  le2msq  7865  msq11  7866  ledivp1  7867  peano5uzti  8344  eluzuzle  8479  qreccl  8574  xrltso  8715  z2ge  8737  ixxss1  8771  ixxss2  8772  elioc2  8803  divelunit  8868  fzass4  8923  fzrev  8944  fzonmapblen  9041  elfzodifsumelfzo  9055  ssfzo12bi  9079  qbtwnzlemstep  9101  qbtwnzlemex  9103  rebtwn2z  9107  expivallem  9230  expp1  9236  expcl2lemap  9241  expnegzap  9263  expadd  9271  expmul  9274  leexp1a  9283  expnlbnd  9347  shftfvalg  9393  shftfval  9396  caucvgrelemrec  9552  resqrexlemdecn  9584  sqrtmul  9607  sqrtdiv  9614  leabs  9646  absexpzap  9650  ltabs  9657  abslt  9658  absle  9659  abssubap0  9660  amgm2  9688  icodiamlt  9750  qdenre  9772  climuni  9788  cn1lem  9808  iiserex  9833  iserile  9836  climcau  9840  sqrt2irr  9852  qdencn  10097
  Copyright terms: Public domain W3C validator