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

Theorem simp2r 931
 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 926 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885 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 887 This theorem is referenced by:  simpl2r  958  simpr2r  964  simp12r  1018  simp22r  1024  simp32r  1030  issod  4056  funprg  4949  fsnunf  5362  f1oiso2  5466  tfrlemibxssdm  5941  ecopovtrn  6203  ecopovtrng  6206  addassnqg  6480  ltsonq  6496  ltanqg  6498  ltmnqg  6499  addassnq0  6560  recexprlem1ssl  6731  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltsosr  6849  ltasrg  6855  mulextsr1lem  6864  mulextsr1  6865  axmulass  6947  axdistr  6948  dmdcanap  7698  lediv2  7857  ltdiv23  7858  lediv23  7859  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  expdivap  9305
 Copyright terms: Public domain W3C validator