![]() |
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 998 | . 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: simplr2 1040 simprr2 1046 simp1r2 1094 simp2r2 1100 simp3r2 1106 3anandis 1347 isopolem 5822 tfrlemibacc 6326 tfrlemibfn 6328 tfr1onlembacc 6342 tfr1onlembfn 6344 tfrcllembacc 6355 tfrcllembfn 6357 prltlu 7485 prdisj 7490 prmuloc2 7565 ltntri 8083 eluzuzle 9534 xlesubadd 9881 elioc2 9934 elico2 9935 elicc2 9936 fseq1p1m1 10091 fz0fzelfz0 10124 seq3f1olemp 10499 bcval5 10738 hashdifpr 10795 summodclem2 11385 isumss2 11396 tanaddap 11742 dvds2ln 11826 divalglemeunn 11920 divalglemex 11921 divalglemeuneg 11922 isstructr 12471 f1ovscpbl 12715 mndissubm 12820 grpsubrcan 12905 grpsubadd 12912 grpaddsubass 12914 grpsubsub4 12917 grppnpcan2 12918 grpnpncan 12919 mulgnndir 12965 mulgnn0dir 12966 mulgdir 12968 mulgnnass 12971 mulgnn0ass 12972 mulgass 12973 mulgsubdir 12976 issubg2m 13002 eqgval 13035 cmn32 13060 cmn12 13062 abladdsub 13071 ablsubsub23 13081 srgdilem 13105 srgass 13107 ringdilem 13148 ringass 13152 opprring 13202 mulgass3 13207 unitgrp 13238 dvrass 13261 dvrdir 13265 aprap 13297 subrgunit 13320 issubrg2 13322 restopnb 13574 icnpimaex 13604 cnptopresti 13631 psmettri 13723 isxmet2d 13741 xmettri 13765 metrtri 13770 xmetres2 13772 bldisj 13794 blss2ps 13799 blss2 13800 xmstri2 13863 mstri2 13864 xmstri 13865 mstri 13866 xmstri3 13867 mstri3 13868 msrtri 13869 comet 13892 bdbl 13896 xmetxp 13900 dvconst 14054 |
Copyright terms: Public domain | W3C validator |