Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpr1 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 981 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | adantl 275 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
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 964 |
This theorem is referenced by: simplr1 1023 simprr1 1029 simp1r1 1077 simp2r1 1083 simp3r1 1089 3anandis 1325 isopolem 5723 caovlem2d 5963 tfrlemibacc 6223 tfrlemibfn 6225 tfr1onlembacc 6239 tfr1onlembfn 6241 tfrcllembacc 6252 tfrcllembfn 6254 eqsupti 6883 prmuloc2 7375 ltntri 7890 elioc2 9719 elico2 9720 elicc2 9721 fseq1p1m1 9874 elfz0ubfz0 9902 ico0 10039 seq3f1olemp 10275 seq3f1oleml 10276 bcval5 10509 isumss2 11162 tanaddap 11446 dvds2ln 11526 divalglemeunn 11618 divalglemex 11619 divalglemeuneg 11620 qredeq 11777 isstructr 11974 icnpimaex 12380 cnptopresti 12407 upxp 12441 psmettri 12499 isxmet2d 12517 xmettri 12541 metrtri 12546 xmetres2 12548 bldisj 12570 blss2ps 12575 blss2 12576 xmstri2 12639 mstri2 12640 xmstri 12641 mstri 12642 xmstri3 12643 mstri3 12644 msrtri 12645 comet 12668 bdbl 12672 xmetxp 12676 dvconst 12830 findset 13143 |
Copyright terms: Public domain | W3C validator |