![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpr2 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 963 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒) | |
2 | 1 | adantl 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 |