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

Theorem simpl3 909
 Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl3 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 906 . 2 ((𝜑𝜓𝜒) → 𝜒)
21adantr 261 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  simpll3  945  simprl3  951  simp1l3  999  simp2l3  1005  simp3l3  1011  3anandirs  1238  frirrg  4087  fcofo  5424  acexmid  5511  oawordi  6049  nnmord  6090  nnmword  6091  fidifsnen  6331  dif1en  6337  ac6sfi  6352  enq0tr  6532  distrlem4prl  6682  distrlem4pru  6683  ltaprg  6717  lelttr  7106  ltletr  7107  readdcan  7153  addcan  7191  addcan2  7192  ltadd2  7416  xrlelttr  8722  xrltletr  8723  icoshftf1o  8859  difelfzle  8992  fzo1fzo0n0  9039  ltexp2a  9306  exple1  9310  expnlbnd2  9374  addcn2  9831  mulcn2  9833
 Copyright terms: Public domain W3C validator