![]() |
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 997 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | adantl 277 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: simplr1 1039 simprr1 1045 simp1r1 1093 simp2r1 1099 simp3r1 1105 3anandis 1347 isopolem 5822 caovlem2d 6066 tfrlemibacc 6326 tfrlemibfn 6328 tfr1onlembacc 6342 tfr1onlembfn 6344 tfrcllembacc 6355 tfrcllembfn 6357 eqsupti 6994 prmuloc2 7565 ltntri 8084 elioc2 9935 elico2 9936 elicc2 9937 fseq1p1m1 10093 elfz0ubfz0 10124 ico0 10261 seq3f1olemp 10501 seq3f1oleml 10502 bcval5 10742 isumss2 11400 tanaddap 11746 dvds2ln 11830 divalglemeunn 11925 divalglemex 11926 divalglemeuneg 11927 qredeq 12095 pcdvdstr 12325 isstructr 12476 mndissubm 12865 grpsubrcan 12950 grpsubadd 12957 grpsubsub 12958 grpaddsubass 12959 grpsubsub4 12962 grpnnncan2 12966 mulgnndir 13010 mulgnn0dir 13011 mulgdir 13013 mulgnnass 13016 mulgnn0ass 13017 mulgass 13018 mulgsubdir 13021 issubg2m 13047 eqgval 13080 cmn32 13105 cmn12 13107 abladdsub 13116 srgass 13152 ringdilem 13193 ringass 13197 opprring 13247 mulgass3 13252 unitgrp 13283 dvrass 13306 dvrdir 13310 aprap 13342 subrgunit 13365 issubrg2 13367 icnpimaex 13647 cnptopresti 13674 upxp 13708 psmettri 13766 isxmet2d 13784 xmettri 13808 metrtri 13813 xmetres2 13815 bldisj 13837 blss2ps 13842 blss2 13843 xmstri2 13906 mstri2 13907 xmstri 13908 mstri 13909 xmstri3 13910 mstri3 13911 msrtri 13912 comet 13935 bdbl 13939 xmetxp 13943 dvconst 14097 findset 14633 |
Copyright terms: Public domain | W3C validator |