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  1004  simp2ll  1008  simp3ll  1012  rmob  2920  prneimg  3603  exmid01  4008  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  poinxp  4477  mpteqb  5358  fvmptt  5359  fcof1  5525  acexmid  5614  grprinvlem  5798  dftpos4  5984  tfrlem3ag  6030  tfrlem3a  6031  tfrlemi1  6053  tfrexlem  6055  tfr1onlem3ag  6058  dcdifsnid  6219  qsel  6323  ecopovsymg  6345  ecopoverg  6347  th3qlem1  6348  mapss  6402  xpmapenlem  6519  findcard2  6559  findcard2s  6560  findcard2sd  6562  unfiin  6590  f1finf1o  6608  sbthlemi6  6618  sbthlemi8  6620  supisolem  6650  dfplpq2  6860  dfmpq2  6861  mulpipqqs  6879  distrnqg  6893  ltexnqq  6914  subhalfnqq  6920  prarloclemarch  6924  nnnq0lem1  6952  distrnq0  6965  npsspw  6977  prarloclemlo  7000  prarloclem3  7003  prarloclemcalc  7008  genplt2i  7016  distrlem1prl  7088  distrlem1pru  7089  distrlem4prl  7090  distrlem4pru  7091  ltprordil  7095  ltexprlemlol  7108  ltexprlemupu  7110  addextpr  7127  recexprlemopl  7131  recexprlemdisj  7136  recexprlem1ssl  7139  aptiprleml  7145  prsrlem1  7235  recexgt0sr  7266  addcnsr  7318  mulcnsr  7319  mulcnsrec  7327  axaddcl  7348  axmulcl  7350  axmulcom  7353  rereceu  7371  cnegexlem1  7604  cnegex  7607  addsub4  7672  le2add  7869  lt2add  7870  lt2sub  7885  le2sub  7886  rereim  8007  apreim  8024  mulreim  8025  addext  8031  mulext  8035  receuap  8080  rec11ap  8119  rec11rap  8120  divdivdivap  8122  ddcanap  8135  divadddivap  8136  divsubdivap  8137  conjmulap  8138  rerecclap  8139  recgt0  8249  prodgt0gt0  8250  prodgt0  8251  prodge0  8253  ltmul12a  8259  lemul12a  8261  lemulge11  8265  lt2mul2div  8278  ltrec  8282  lerec  8283  lt2msq  8285  ltrec1  8287  le2msq  8300  msq11  8301  ledivp1  8302  mulle0r  8343  peano5uzti  8790  eluzuzle  8962  qreccl  9062  xrltso  9201  z2ge  9223  ixxss1  9257  ixxss2  9258  elioc2  9289  divelunit  9354  fzass4  9410  fzrev  9431  fzonmapblen  9529  elfzodifsumelfzo  9543  ssfzo12bi  9567  rebtwn2z  9597  qbtwnxr  9600  modqid  9687  modqcyc  9697  modqaddabs  9700  modqaddmod  9701  mulqaddmodid  9702  modqadd2mod  9712  modqltm1p1mod  9714  modqsubmod  9720  modqsubmodmod  9721  modqmulmod  9727  modqmulmodr  9728  modqsubdir  9731  frecuzrdgg  9754  iseqvalt  9793  iseqf1olemp  9839  expivallem  9858  expp1  9864  expcl2lemap  9869  expnegzap  9891  expadd  9899  expmul  9902  leexp1a  9912  expnlbnd  9978  nn0opth2  10032  bcval  10057  ibcval5  10071  bcpasc  10074  hashunsng  10115  iseqcoll  10147  shftfvalg  10152  shftfval  10155  caucvgrelemrec  10311  resqrexlemdecn  10344  sqrtmul  10367  sqrtdiv  10374  leabs  10406  absexpzap  10412  ltabs  10419  abslt  10420  absle  10421  abssubap0  10422  amgm2  10450  icodiamlt  10512  qdenre  10534  maxleim  10537  maxleastlt  10547  rexico  10553  zmaxcl  10555  minmax  10559  climuni  10579  cn1lem  10599  iiserex  10624  iserile  10627  climcau  10631  isummolem2a  10665  isummo  10667  isumss  10674  fisumss  10675  fsumadd  10688  zdvdsdc  10723  dvds2ln  10735  dvdsle  10751  divconjdvds  10756  dvdsext  10762  gcdsupex  10855  gcdsupcl  10856  bezoutlemmain  10893  bezoutlemaz  10898  bezoutlembi  10900  bezout  10906  gcdmultiplez  10916  dvdsmulgcd  10920  bezoutr  10927  bezoutr1  10928  lcmval  10951  lcmcllem  10955  ncoprmgcdne1b  10977  cncongr1  10991  prmdvdsexp  11033  sqrt2irr  11047  pw2dvdslemn  11049  pw2dvdseu  11052  nonsq  11091  nninfalllem1  11368  nninfsellemqall  11376  qdencn  11384
  Copyright terms: Public domain W3C validator