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

Theorem simpl3 908
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl3 (((φ ψ χ) θ) → χ)

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 905 . 2 ((φ ψ χ) → χ)
21adantr 261 1 (((φ ψ χ) θ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
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 886
This theorem is referenced by:  simpll3  944  simprl3  950  simp1l3  998  simp2l3  1004  simp3l3  1010  3anandirs  1237  fcofo  5367  acexmid  5454  oawordi  5988  nnmord  6026  nnmword  6027  enq0tr  6416  distrlem4prl  6559  distrlem4pru  6560  ltaprg  6591  lelttr  6883  ltletr  6884  readdcan  6930  addcan  6968  addcan2  6969  ltadd2  7192  xrlelttr  8472  xrltletr  8473  icoshftf1o  8609  difelfzle  8742  fzo1fzo0n0  8789  ltexp2a  8940  exple1  8944  expnlbnd2  9007
  Copyright terms: Public domain W3C validator