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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 109 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 988 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  simpl2r  1020  simpr2r  1026  simp12r  1080  simp22r  1086  simp32r  1092  issod  4211  funprg  5143  fsnunf  5588  f1oiso2  5696  tfrlemibxssdm  6192  ecopovtrn  6494  ecopovtrng  6497  addassnqg  7158  ltsonq  7174  ltanqg  7176  ltmnqg  7177  addassnq0  7238  recexprlem1ssl  7409  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1lem  7556  mulextsr1  7557  axmulass  7649  axdistr  7650  dmdcanap  8450  lediv2  8617  ltdiv23  8618  lediv23  8619  xaddass2  9621  xlt2add  9631  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  expdivap  10312  leisorel  10548  bdtrilem  10978  xrbdtri  11013  fldivndvdslt  11559  prmexpb  11756  cnptoprest  12335  ssblps  12521  ssbl  12522  tgqioo  12643
  Copyright terms: Public domain W3C validator