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

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

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 964 . 2 ((𝜓𝜒𝜃) → 𝜓)
21adantl 273 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simplr1  1006  simprr1  1012  simp1r1  1060  simp2r1  1066  simp3r1  1072  3anandis  1308  isopolem  5689  caovlem2d  5929  tfrlemibacc  6189  tfrlemibfn  6191  tfr1onlembacc  6205  tfr1onlembfn  6207  tfrcllembacc  6218  tfrcllembfn  6220  eqsupti  6849  prmuloc2  7339  ltntri  7854  elioc2  9670  elico2  9671  elicc2  9672  fseq1p1m1  9825  elfz0ubfz0  9853  ico0  9990  seq3f1olemp  10226  seq3f1oleml  10227  bcval5  10460  isumss2  11113  tanaddap  11356  dvds2ln  11433  divalglemeunn  11525  divalglemex  11526  divalglemeuneg  11527  qredeq  11684  isstructr  11880  icnpimaex  12286  cnptopresti  12313  upxp  12347  psmettri  12405  isxmet2d  12423  xmettri  12447  metrtri  12452  xmetres2  12454  bldisj  12476  blss2ps  12481  blss2  12482  xmstri2  12545  mstri2  12546  xmstri  12547  mstri  12548  xmstri3  12549  mstri3  12550  msrtri  12551  comet  12574  bdbl  12578  xmetxp  12582  dvconst  12736  findset  12977
  Copyright terms: Public domain W3C validator