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

Theorem simp1r 928
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1r (((φ ψ) χ θ) → ψ)

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 103 . 2 ((φ ψ) → ψ)
213ad2ant1 924 1 (((φ ψ) χ θ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
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 depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simpl1r  955  simpr1r  961  simp11r  1015  simp21r  1021  simp31r  1027  vtoclgft  2598  en2lp  4232  funprg  4892  nnsucsssuc  6010  ecopovtrn  6139  ecopovtrng  6142  addassnqg  6366  distrnqg  6371  ltsonq  6382  ltanqg  6384  ltmnqg  6385  distrnq0  6441  addassnq0  6444  prarloclem5  6482  recexprlem1ssl  6604  recexprlem1ssu  6605  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltsosr  6672  ltasrg  6678  mulextsr1lem  6686  mulextsr1  6687  axmulass  6737  axdistr  6738  dmdcanap  7460  lt2msq1  7612  lediv2  7618  expaddzaplem  8932  expaddzap  8933  expmulzap  8935
  Copyright terms: Public domain W3C validator