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

Theorem simp2r 940
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2r ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 107 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 935 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  simpl2r  967  simpr2r  973  simp12r  1027  simp22r  1033  simp32r  1039  issod  4081  funprg  4974  fsnunf  5387  f1oiso2  5491  tfrlemibxssdm  5969  ecopovtrn  6231  ecopovtrng  6234  addassnqg  6508  ltsonq  6524  ltanqg  6526  ltmnqg  6527  addassnq0  6588  recexprlem1ssl  6759  mulasssrg  6871  distrsrg  6872  lttrsr  6875  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892  mulextsr1  6893  axmulass  6975  axdistr  6976  dmdcanap  7743  lediv2  7902  ltdiv23  7903  lediv23  7904  expaddzaplem  9428  expaddzap  9429  expmulzap  9431  expdivap  9436
  Copyright terms: Public domain W3C validator