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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 103 . 2 ((ψ χ) → χ)
213ad2ant2 925 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:  simpl2r  957  simpr2r  963  simp12r  1017  simp22r  1023  simp32r  1029  issod  4047  funprg  4892  fsnunf  5305  f1oiso2  5409  tfrlemibxssdm  5882  ecopovtrn  6139  ecopovtrng  6142  addassnqg  6366  ltsonq  6382  ltanqg  6384  ltmnqg  6385  addassnq0  6444  recexprlem1ssl  6604  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltsosr  6672  ltasrg  6678  mulextsr1lem  6686  mulextsr1  6687  axmulass  6737  axdistr  6738  dmdcanap  7460  lediv2  7618  ltdiv23  7619  lediv23  7620  expaddzaplem  8932  expaddzap  8933  expmulzap  8935  expdivap  8939
 Copyright terms: Public domain W3C validator