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

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

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 894 . 2 ((φ ψ χ) → χ)
21adantr 261 1 (((φ ψ χ) θ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
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 875
This theorem is referenced by:  simpll3  933  simprl3  939  simp1l3  987  simp2l3  993  simp3l3  999  3anandirs  1223  fcofo  5349  acexmid  5435  oawordi  5964  nnmord  6001  nnmword  6002  enq0tr  6289  distrlem4prl  6423  distrlem4pru  6424  ltaprg  6455  lelttr  6704  ltletr  6705  readdcan  6746  addcan  6784  addcan2  6785  ltadd2  7008
  Copyright terms: Public domain W3C validator