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

Theorem simprr 484
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 460 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  969  simp2rr  973  simp3rr  977  fvmptt  5205  fcof1  5366  fliftfun  5379  isotr  5399  riotass2  5437  acexmidlemab  5449  ovmpt2df  5574  grprinvlem  5637  1stconst  5784  2ndconst  5785  cnvf1olem  5787  smoiso  5858  swoer  6070  erinxp  6116  ecopovsymg  6141  th3qlem1  6144  f1imaen2g  6209  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  enq0sym  6414  enq0tr  6416  distrnq0  6441  prarloclem3  6479  genplt2i  6492  addlocpr  6519  prmuloc  6545  distrlem1prl  6556  distrlem1pru  6557  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  ltaprg  6590  addextpr  6591  recexprlemdisj  6600  recexprlemloc  6601  aptiprleml  6609  aptiprlemu  6610  ltmprr  6612  archpr  6613  recexgt0sr  6661  mulgt0sr  6664  addcnsr  6691  mulcnsr  6692  mulcnsrec  6700  axmulcom  6715  axarch  6733  lelttr  6863  ltletr  6864  addcan  6948  addcan2  6949  addsub4  7010  ltadd2  7172  le2add  7194  lt2add  7195  lt2sub  7210  le2sub  7211  rereim  7330  apreap  7331  apreim  7347  mulreim  7348  apcotr  7351  apadd1  7352  addext  7354  apneg  7355  mulext1  7356  mulext  7358  ltleap  7373  mulap0  7377  mulcanapd  7384  rec11ap  7428  rec11rap  7429  divdivdivap  7431  ddcanap  7444  divadddivap  7445  prodgt0gt0  7558  prodgt0  7559  prodge0  7561  lemulge11  7573  lt2mul2div  7586  ltrec  7590  lerec  7591  lerec2  7596  ledivp1  7610  nn0ge0div  8063  qapne  8310  xrlelttr  8452  xrltletr  8453  xrre3  8465  xrrege0  8468  fzass4  8655  fzrev  8676  elfz1b  8682  eluzgtdifelfzo  8783  fzocatel  8785  frec2uzisod  8834  iseqovex  8859  iseqval  8860  expnegzap  8903  ltexp2a  8920  le2sq2  8942  bernneq  8982  expnlbnd2  8987
  Copyright terms: Public domain W3C validator