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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 108 . 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:  simpl2l  1019  simpr2l  1025  simp12l  1079  simp22l  1085  simp32l  1091  issod  4211  funprg  5143  fsnunf  5588  f1oiso2  5696  ecopovtrn  6494  ecopovtrng  6497  addassnqg  7158  ltsonq  7174  ltanqg  7176  ltmnqg  7177  addassnq0  7238  recexprlem1ssu  7410  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1lem  7556  mulextsr1  7557  axmulass  7649  axdistr  7650  dmdcanap  8450  ltdiv2  8613  lediv2  8617  ltdiv23  8618  lediv23  8619  xaddass  9620  xaddass2  9621  xlt2add  9631  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  expdivap  10312  leisorel  10548  bdtrilem  10978  bdtri  10979  xrbdtri  11013  fsumsplitsnun  11156  prmexpb  11756  cnptoprest  12335  ssblps  12521  ssbl  12522  tgqioo  12643
  Copyright terms: Public domain W3C validator