ILE Home 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  6530  distrlem4prl  6680  distrlem4pru  6681  ltaprg  6715  lelttr  7104  ltletr  7105  readdcan  7151  addcan  7189  addcan2  7190  ltadd2  7414  xrlelttr  8720  xrltletr  8721  icoshftf1o  8857  difelfzle  8990  fzo1fzo0n0  9037  ltexp2a  9304  exple1  9308  expnlbnd2  9372  addcn2  9829  mulcn2  9831
  Copyright terms: Public domain W3C validator