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

Theorem simp2r 968
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 963 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 924
This theorem is referenced by:  simpl2r  995  simpr2r  1001  simp12r  1055  simp22r  1061  simp32r  1067  issod  4120  funprg  5029  fsnunf  5459  f1oiso2  5567  tfrlemibxssdm  6046  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  ltsonq  6901  ltanqg  6903  ltmnqg  6904  addassnq0  6965  recexprlem1ssl  7136  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  dmdcanap  8128  lediv2  8287  ltdiv23  8288  lediv23  8289  expaddzaplem  9896  expaddzap  9897  expmulzap  9899  expdivap  9904  leisorel  10138  fldivndvdslt  10810  prmexpb  11005
  Copyright terms: Public domain W3C validator