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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 967 . 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:  simplr2  1009  simprr2  1015  simp1r2  1063  simp2r2  1069  simp3r2  1075  3anandis  1310  isopolem  5691  tfrlemibacc  6191  tfrlemibfn  6193  tfr1onlembacc  6207  tfr1onlembfn  6209  tfrcllembacc  6220  tfrcllembfn  6222  prltlu  7263  prdisj  7268  prmuloc2  7343  ltntri  7858  eluzuzle  9302  xlesubadd  9634  elioc2  9687  elico2  9688  elicc2  9689  fseq1p1m1  9842  fz0fzelfz0  9872  seq3f1olemp  10243  bcval5  10477  hashdifpr  10534  summodclem2  11119  isumss2  11130  tanaddap  11373  dvds2ln  11453  divalglemeunn  11545  divalglemex  11546  divalglemeuneg  11547  isstructr  11901  restopnb  12277  icnpimaex  12307  cnptopresti  12334  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
  Copyright terms: Public domain W3C validator