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

Theorem simpll 496
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )

Proof of Theorem simpll
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
21ad2antrr 472 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
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  3601  exmid01  4005  ordtri2or2exmidlem  4314  onsucelsucexmidlem  4317  poinxp  4474  mpteqb  5350  fvmptt  5351  fcof1  5517  acexmid  5606  grprinvlem  5790  dftpos4  5976  tfrlem3ag  6022  tfrlem3a  6023  tfrlemi1  6045  tfrexlem  6047  tfr1onlem3ag  6050  dcdifsnid  6211  qsel  6315  ecopovsymg  6337  ecopoverg  6339  th3qlem1  6340  mapss  6394  xpmapenlem  6511  findcard2  6551  findcard2s  6552  findcard2sd  6554  unfiin  6582  f1finf1o  6599  sbthlemi6  6608  sbthlemi8  6610  supisolem  6640  dfplpq2  6850  dfmpq2  6851  mulpipqqs  6869  distrnqg  6883  ltexnqq  6904  subhalfnqq  6910  prarloclemarch  6914  nnnq0lem1  6942  distrnq0  6955  npsspw  6967  prarloclemlo  6990  prarloclem3  6993  prarloclemcalc  6998  genplt2i  7006  distrlem1prl  7078  distrlem1pru  7079  distrlem4prl  7080  distrlem4pru  7081  ltprordil  7085  ltexprlemlol  7098  ltexprlemupu  7100  addextpr  7117  recexprlemopl  7121  recexprlemdisj  7126  recexprlem1ssl  7129  aptiprleml  7135  prsrlem1  7225  recexgt0sr  7256  addcnsr  7308  mulcnsr  7309  mulcnsrec  7317  axaddcl  7338  axmulcl  7340  axmulcom  7343  rereceu  7361  cnegexlem1  7594  cnegex  7597  addsub4  7662  le2add  7859  lt2add  7860  lt2sub  7875  le2sub  7876  rereim  7997  apreim  8014  mulreim  8015  addext  8021  mulext  8025  receuap  8070  rec11ap  8109  rec11rap  8110  divdivdivap  8112  ddcanap  8125  divadddivap  8126  divsubdivap  8127  conjmulap  8128  rerecclap  8129  recgt0  8239  prodgt0gt0  8240  prodgt0  8241  prodge0  8243  ltmul12a  8249  lemul12a  8251  lemulge11  8255  lt2mul2div  8268  ltrec  8272  lerec  8273  lt2msq  8275  ltrec1  8277  le2msq  8290  msq11  8291  ledivp1  8292  mulle0r  8333  peano5uzti  8780  eluzuzle  8952  qreccl  9052  xrltso  9191  z2ge  9213  ixxss1  9247  ixxss2  9248  elioc2  9279  divelunit  9344  fzass4  9400  fzrev  9421  fzonmapblen  9519  elfzodifsumelfzo  9533  ssfzo12bi  9557  rebtwn2z  9587  qbtwnxr  9590  modqid  9677  modqcyc  9687  modqaddabs  9690  modqaddmod  9691  mulqaddmodid  9692  modqadd2mod  9702  modqltm1p1mod  9704  modqsubmod  9710  modqsubmodmod  9711  modqmulmod  9717  modqmulmodr  9718  modqsubdir  9721  frecuzrdgg  9744  iseqvalt  9783  iseqf1olemp  9828  expivallem  9847  expp1  9853  expcl2lemap  9858  expnegzap  9880  expadd  9888  expmul  9891  leexp1a  9901  expnlbnd  9967  nn0opth2  10021  bcval  10046  ibcval5  10060  bcpasc  10063  hashunsng  10104  iseqcoll  10136  shftfvalg  10141  shftfval  10144  caucvgrelemrec  10300  resqrexlemdecn  10333  sqrtmul  10356  sqrtdiv  10363  leabs  10395  absexpzap  10401  ltabs  10408  abslt  10409  absle  10410  abssubap0  10411  amgm2  10439  icodiamlt  10501  qdenre  10523  maxleim  10526  maxleastlt  10536  rexico  10542  minmax  10547  climuni  10567  cn1lem  10587  iiserex  10612  iserile  10615  climcau  10619  isummolem2a  10653  isummo  10655  isumss  10662  zdvdsdc  10684  dvds2ln  10696  dvdsle  10712  divconjdvds  10717  dvdsext  10723  gcdsupex  10816  gcdsupcl  10817  bezoutlemmain  10854  bezoutlemaz  10859  bezoutlembi  10861  bezout  10867  gcdmultiplez  10877  dvdsmulgcd  10881  bezoutr  10888  bezoutr1  10889  lcmval  10912  lcmcllem  10916  ncoprmgcdne1b  10938  cncongr1  10952  prmdvdsexp  10994  sqrt2irr  11008  pw2dvdslemn  11010  pw2dvdseu  11013  nonsq  11052  nninfalllem1  11329  nninfsellemqall  11337  qdencn  11345
  Copyright terms: Public domain W3C validator