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

Theorem simpll 496
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 472 1 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simp1ll  1002  simp2ll  1006  simp3ll  1010  rmob  2916  prneimg  3587  exmid01  3989  ordtri2or2exmidlem  4298  onsucelsucexmidlem  4301  poinxp  4456  mpteqb  5315  fvmptt  5316  fcof1  5476  acexmid  5564  grprinvlem  5748  dftpos4  5934  tfrlem3ag  5980  tfrlem3a  5981  tfrlemi1  6003  tfrexlem  6005  tfr1onlem3ag  6008  dcdifsnid  6168  qsel  6272  ecopovsymg  6294  ecopoverg  6296  th3qlem1  6297  findcard2  6447  findcard2s  6448  findcard2sd  6450  unfiin  6472  f1finf1o  6488  supisolem  6517  dfplpq2  6683  dfmpq2  6684  mulpipqqs  6702  distrnqg  6716  ltexnqq  6737  subhalfnqq  6743  prarloclemarch  6747  nnnq0lem1  6775  distrnq0  6788  npsspw  6800  prarloclemlo  6823  prarloclem3  6826  prarloclemcalc  6831  genplt2i  6839  distrlem1prl  6911  distrlem1pru  6912  distrlem4prl  6913  distrlem4pru  6914  ltprordil  6918  ltexprlemlol  6931  ltexprlemupu  6933  addextpr  6950  recexprlemopl  6954  recexprlemdisj  6959  recexprlem1ssl  6962  aptiprleml  6968  prsrlem1  7058  recexgt0sr  7089  addcnsr  7141  mulcnsr  7142  mulcnsrec  7150  axaddcl  7171  axmulcl  7173  axmulcom  7176  rereceu  7194  cnegexlem1  7427  cnegex  7430  addsub4  7495  le2add  7692  lt2add  7693  lt2sub  7708  le2sub  7709  rereim  7830  apreim  7847  mulreim  7848  addext  7854  mulext  7858  receuap  7903  rec11ap  7942  rec11rap  7943  divdivdivap  7945  ddcanap  7958  divadddivap  7959  divsubdivap  7960  conjmulap  7961  rerecclap  7962  recgt0  8072  prodgt0gt0  8073  prodgt0  8074  prodge0  8076  ltmul12a  8082  lemul12a  8084  lemulge11  8088  lt2mul2div  8101  ltrec  8105  lerec  8106  lt2msq  8108  ltrec1  8110  le2msq  8123  msq11  8124  ledivp1  8125  mulle0r  8166  peano5uzti  8613  eluzuzle  8785  qreccl  8885  xrltso  9024  z2ge  9046  ixxss1  9080  ixxss2  9081  elioc2  9112  divelunit  9177  fzass4  9233  fzrev  9254  fzonmapblen  9350  elfzodifsumelfzo  9364  ssfzo12bi  9388  rebtwn2z  9418  qbtwnxr  9421  modqid  9508  modqcyc  9518  modqaddabs  9521  modqaddmod  9522  mulqaddmodid  9523  modqadd2mod  9533  modqltm1p1mod  9535  modqsubmod  9541  modqsubmodmod  9542  modqmulmod  9548  modqmulmodr  9549  modqsubdir  9552  frecuzrdgg  9575  iseqvalt  9609  expivallem  9651  expp1  9657  expcl2lemap  9662  expnegzap  9684  expadd  9692  expmul  9695  leexp1a  9705  expnlbnd  9771  nn0opth2  9825  bcval  9850  ibcval5  9864  bcpasc  9867  hashunsng  9908  shftfvalg  9932  shftfval  9935  caucvgrelemrec  10091  resqrexlemdecn  10124  sqrtmul  10147  sqrtdiv  10154  leabs  10186  absexpzap  10192  ltabs  10199  abslt  10200  absle  10201  abssubap0  10202  amgm2  10230  icodiamlt  10292  qdenre  10314  maxleim  10317  maxleastlt  10327  rexico  10333  minmax  10338  climuni  10358  cn1lem  10378  iiserex  10403  iserile  10406  climcau  10410  zdvdsdc  10449  dvds2ln  10461  dvdsle  10477  divconjdvds  10482  dvdsext  10488  gcdsupex  10581  gcdsupcl  10582  bezoutlemmain  10619  bezoutlemaz  10624  bezoutlembi  10626  bezout  10632  gcdmultiplez  10642  dvdsmulgcd  10646  bezoutr  10653  bezoutr1  10654  lcmval  10677  lcmcllem  10681  ncoprmgcdne1b  10703  cncongr1  10717  prmdvdsexp  10759  sqrt2irr  10773  pw2dvdslemn  10775  pw2dvdseu  10778  nonsq  10817  qdencn  11077
  Copyright terms: Public domain W3C validator