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

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

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 966 . 2 ((𝜓𝜒𝜃) → 𝜓)
21adantl 275 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
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 949
This theorem is referenced by:  simplr1  1008  simprr1  1014  simp1r1  1062  simp2r1  1068  simp3r1  1074  3anandis  1310  isopolem  5691  caovlem2d  5931  tfrlemibacc  6191  tfrlemibfn  6193  tfr1onlembacc  6207  tfr1onlembfn  6209  tfrcllembacc  6220  tfrcllembfn  6222  eqsupti  6851  prmuloc2  7343  ltntri  7858  elioc2  9687  elico2  9688  elicc2  9689  fseq1p1m1  9842  elfz0ubfz0  9870  ico0  10007  seq3f1olemp  10243  seq3f1oleml  10244  bcval5  10477  isumss2  11130  tanaddap  11373  dvds2ln  11453  divalglemeunn  11545  divalglemex  11546  divalglemeuneg  11547  qredeq  11704  isstructr  11901  icnpimaex  12307  cnptopresti  12334  upxp  12368  psmettri  12426  isxmet2d  12444  xmettri  12468  metrtri  12473  xmetres2  12475  bldisj  12497  blss2ps  12502  blss2  12503  xmstri2  12566  mstri2  12567  xmstri  12568  mstri  12569  xmstri3  12570  mstri3  12571  msrtri  12572  comet  12595  bdbl  12599  xmetxp  12603  dvconst  12757  findset  13070
  Copyright terms: Public domain W3C validator