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

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

Proof of Theorem simprr
StepHypRef Expression
1 id 19 . 2 (χχ)
21ad2antll 464 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:  simp1rr  956  simp2rr  960  simp3rr  964  fvmptt  5183  fcof1  5344  fliftfun  5357  isotr  5377  riotass2  5414  acexmidlemab  5426  ovmpt2df  5551  grprinvlem  5614  1stconst  5761  2ndconst  5762  cnvf1olem  5764  smoiso  5835  swoer  6041  erinxp  6087  ecopovsymg  6112  th3qlem1  6115  dfplpq2  6207  dfmpq2  6208  mulpipqqs  6226  distrnqg  6240  enq0sym  6281  enq0tr  6283  distrnq0  6308  prarloclem3  6345  genplt2i  6358  addlocpr  6385  prmuloc  6404  distrlem1prl  6415  distrlem1pru  6416  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  ltaprg  6449  recexprlemdisj  6458  recexprlemloc  6459  aptiprleml  6467  aptiprlemu  6468  recexgt0sr  6517  mulgt0sr  6520  addcnsr  6544  mulcnsr  6545  mulcnsrec  6553  axmulcom  6564  lelttr  6708  ltletr  6709  addcan  6793  addcan2  6794  addsub4  6855  ltadd2  7017  le2add  7039  lt2add  7040  lt2sub  7055  le2sub  7056  rereim  7175  apreap  7176  apreim  7188  apcotr  7191  apadd1  7192  extadd  7194  apneg  7195
  Copyright terms: Public domain W3C validator