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

Theorem simprl 483
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprl ((φ (ψ χ)) → ψ)

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2 (ψψ)
21ad2antrl 459 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:  simp1rl  968  simp2rl  972  simp3rl  976  rmob  2844  0xp  4363  imainss  4682  fvmptt  5205  fcof1o  5372  isotr  5399  riota5f  5435  ovmpt2df  5574  grprinvlem  5637  grpridd  5639  unielxp  5742  1stconst  5784  2ndconst  5785  cnvf1olem  5787  tfrlemi14d  5888  tfrexlem  5889  nnaordi  6017  swoer  6070  qliftfun  6124  ecopovsymg  6141  th3qlem1  6144  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  ltexnqq  6391  subhalfnqq  6397  distrnq0  6442  prarloclemup  6478  prarloclem3  6480  prarloc  6486  genplt2i  6493  nqprl  6533  prmuloc  6547  mullocpr  6552  distrlem4prl  6560  distrlem4pru  6561  ltaddpr  6571  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltaprlem  6591  ltaprg  6592  addextpr  6593  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  caucvgprlemnkj  6637  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlem2  6651  recexgt0sr  6701  mulgt0sr  6704  addcnsr  6731  mulcnsr  6732  mulcnsrec  6740  axaddcl  6750  axmulcl  6752  axmulcom  6755  lelttr  6903  ltletr  6904  readdcan  6950  addcan  6988  addcan2  6989  addsub4  7050  ltadd2  7212  le2add  7234  lt2add  7235  lt2sub  7250  le2sub  7251  rimul  7369  rereim  7370  ltmul1  7376  apreim  7387  mulreim  7388  apcotr  7391  apadd1  7392  addext  7394  apneg  7395  mulext1  7396  mulext  7398  ltleap  7413  mulap0  7417  mulcanapd  7424  receuap  7432  rec11ap  7468  rec11rap  7469  divdivdivap  7471  ddcanap  7484  divadddivap  7485  conjmulap  7487  prodgt0gt0  7598  prodge0  7601  ltmul12a  7607  lemulge11  7613  lt2mul2div  7626  ltrec  7630  lerec  7631  lt2msq  7633  lerec2  7636  le2msq  7648  msq11  7649  ledivp1  7650  peano5uzti  8122  qapne  8350  xrlelttr  8492  xrltletr  8493  xrre  8503  divelunit  8640  fzass4  8695  fzocatel  8825  frec2uzisod  8874  iseqovex  8899  iseqval  8900  iseqfveq2  8905  expivallem  8910  expcl2lemap  8921  expnegzap  8943  ltexp2a  8960  le2sq2  8982  sqrtsq  9214
  Copyright terms: Public domain W3C validator