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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 963 . 2 ((𝜓𝜒𝜃) → 𝜒)
21adantl 273 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 945
This theorem is referenced by:  simplr2  1005  simprr2  1011  simp1r2  1059  simp2r2  1065  simp3r2  1071  3anandis  1306  isopolem  5675  tfrlemibacc  6175  tfrlemibfn  6177  tfr1onlembacc  6191  tfr1onlembfn  6193  tfrcllembacc  6204  tfrcllembfn  6206  prltlu  7237  prdisj  7242  prmuloc2  7317  ltntri  7807  eluzuzle  9230  xlesubadd  9553  elioc2  9606  elico2  9607  elicc2  9608  fseq1p1m1  9761  fz0fzelfz0  9791  seq3f1olemp  10162  bcval5  10396  hashdifpr  10453  summodclem2  11037  isumss2  11048  tanaddap  11291  dvds2ln  11368  divalglemeunn  11460  divalglemex  11461  divalglemeuneg  11462  isstructr  11811  restopnb  12187  icnpimaex  12216  cnptopresti  12243  psmettri  12313  isxmet2d  12331  xmettri  12355  metrtri  12360  xmetres2  12362  bldisj  12384  blss2ps  12389  blss2  12390  xmstri2  12453  mstri2  12454  xmstri  12455  mstri  12456  xmstri3  12457  mstri3  12458  msrtri  12459  comet  12482  bdbl  12486  xmetxp  12490  dvconst  12610
  Copyright terms: Public domain W3C validator