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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 108 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 961 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115  df-3an 922 This theorem is referenced by:  simpl2r  993  simpr2r  999  simp12r  1053  simp22r  1059  simp32r  1065  issod  4082  funprg  4980  fsnunf  5394  f1oiso2  5497  tfrlemibxssdm  5976  ecopovtrn  6269  ecopovtrng  6272  addassnqg  6634  ltsonq  6650  ltanqg  6652  ltmnqg  6653  addassnq0  6714  recexprlem1ssl  6885  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  mulextsr1lem  7018  mulextsr1  7019  axmulass  7101  axdistr  7102  dmdcanap  7877  lediv2  8036  ltdiv23  8037  lediv23  8038  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  expdivap  9624  fldivndvdslt  10479  prmexpb  10674
 Copyright terms: Public domain W3C validator