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

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

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
21ad2antrl 474 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ps )
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:  simp1rl  1004  simp2rl  1008  simp3rl  1012  rmob  2915  reg3exmidlemwe  4349  0xp  4466  imainss  4789  fvmptt  5315  fcof1o  5481  isotr  5508  riota5f  5544  ovmpt2df  5684  grprinvlem  5747  grpridd  5749  unielxp  5852  1stconst  5894  2ndconst  5895  cnvf1olem  5897  tfrlemi14d  6003  tfrexlem  6004  tfr1onlemres  6019  tfrcllemres  6032  tfrcldm  6033  frecabcl  6069  nnaordi  6169  swoer  6222  qliftfun  6276  ecopovsymg  6293  th3qlem1  6296  fidifsnen  6427  fisbth  6440  findcard2d  6448  findcard2sd  6449  diffisn  6450  diffifi  6451  ac6sfi  6455  fientri3  6460  nnwetri  6461  unsnfi  6464  unsnfidcex  6465  unsnfidcel  6466  fisseneq  6475  ordiso2  6541  dfplpq2  6676  dfmpq2  6677  mulpipqqs  6695  distrnqg  6709  ltexnqq  6730  subhalfnqq  6736  distrnq0  6781  prarloclemup  6817  prarloclem3  6819  prarloc  6825  genplt2i  6832  nqprl  6873  nqpru  6874  prmuloc  6888  mullocpr  6893  distrlem4prl  6906  distrlem4pru  6907  ltaddpr  6919  ltexprlemopl  6923  ltexprlemlol  6924  ltexprlemopu  6925  ltexprlemupu  6926  ltexprlemrl  6932  ltexprlemru  6934  addcanprleml  6936  addcanprlemu  6937  ltaprlem  6940  ltaprg  6941  prplnqu  6942  addextpr  6943  recexprlemdisj  6952  recexprlemloc  6953  recexprlem1ssl  6955  aptiprleml  6961  aptiprlemu  6962  ltmprr  6964  archpr  6965  cauappcvgprlemopl  6968  cauappcvgprlemopu  6970  cauappcvgprlemdisj  6973  cauappcvgprlemloc  6974  cauappcvgprlem1  6981  cauappcvgprlem2  6982  cauappcvgprlemlim  6983  caucvgprlemnkj  6988  caucvgprlemopl  6991  caucvgprlemopu  6993  caucvgprlemdisj  6996  caucvgprlemloc  6997  caucvgprlem2  7002  caucvgprprlemnkltj  7011  caucvgprprlemnkeqj  7012  caucvgprprlemnjltk  7013  caucvgprprlemmu  7017  caucvgprprlemopl  7019  caucvgprprlemopu  7021  caucvgprprlemdisj  7024  caucvgprprlemloc  7025  caucvgprprlemexbt  7028  caucvgprprlemaddq  7030  caucvgprprlem2  7032  recexgt0sr  7082  mulgt0sr  7086  prsrriota  7096  caucvgsrlemoffres  7108  addcnsr  7134  mulcnsr  7135  mulcnsrec  7143  axaddcl  7164  axmulcl  7166  axmulcom  7169  rereceu  7187  recriota  7188  axcaucvglemres  7197  lelttr  7336  ltletr  7337  readdcan  7385  addcan  7425  addcan2  7426  addsub4  7488  ltadd2  7660  le2add  7685  lt2add  7686  lt2sub  7701  le2sub  7702  rimul  7822  rereim  7823  ltmul1  7829  apreim  7840  mulreim  7841  apcotr  7844  apadd1  7845  addext  7847  apneg  7848  mulext1  7849  mulext  7851  ltleap  7867  mulap0  7881  mulcanapd  7888  receuap  7896  rec11ap  7935  rec11rap  7936  divdivdivap  7938  ddcanap  7951  divadddivap  7952  conjmulap  7954  prodgt0gt0  8066  prodge0  8069  ltmul12a  8075  lemulge11  8081  lt2mul2div  8094  ltrec  8098  lerec  8099  lt2msq  8101  lerec2  8104  le2msq  8116  msq11  8117  ledivp1  8118  mulle0r  8159  suprzclex  8596  peano5uzti  8606  supinfneg  8834  infsupneg  8835  qapne  8875  xrlelttr  9022  xrltletr  9023  xrre  9033  divelunit  9170  fzass4  9226  fzocatel  9355  exbtwnzlemex  9406  rebtwn2z  9411  qbtwnre  9413  modqid  9501  modqcyc  9511  modqaddabs  9514  modqaddmod  9515  mulqaddmodid  9516  modqadd2mod  9526  modqltm1p1mod  9528  modqsubmod  9534  modqsubmodmod  9535  modqmulmod  9541  modqmulmodr  9542  modqaddmulmod  9543  modqsubdir  9545  frec2uzisod  9559  iseqovex  9599  iseqval  9600  iseqfclt  9606  iseqfveq2  9614  iseqshft2  9618  monoord  9621  iseqsplit  9624  iseqid2  9634  iseqdistr  9637  expivallem  9644  expcl2lemap  9655  expnegzap  9677  ltexp2a  9695  le2sq2  9718  nn0opth2  9818  ibcval5  9857  hashcl  9875  hashen  9878  fihashdom  9897  hashunlem  9898  hashun  9899  cvg1nlemres  10090  cvg1n  10091  recvguniq  10100  resqrexlemp1rp  10111  resqrexlemoverl  10126  resqrexlemglsq  10127  resqrexlemex  10130  sqrtmul  10140  sqrtsq  10149  absexpzap  10185  absle  10194  abs3lem  10216  amgm2  10223  maxleastlt  10320  maxltsup  10323  fimaxre2  10328  climcn2  10367  addcn2  10368  mulcn2  10370  climcau  10403  dvdsval2  10424  moddvds  10430  dvdsabseq  10473  dvdsflip  10477  oexpneg  10502  fldivndvdslt  10560  zsupcllemstep  10566  zssinfcl  10569  bezoutlemnewy  10610  bezoutlemstep  10611  bezoutlemeu  10621  dfgcd3  10624  bezout  10625  dvdsmulgcd  10639  bezoutr  10646  ialgrlem1st  10649  lcmgcdlem  10684  coprmdvds2  10700  qredeu  10704  rpdvds  10706  isprm6  10751  pw2dvdslemn  10768  nonsq  10810  crth  10825  qdencn  11070
  Copyright terms: Public domain W3C validator