![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpl2 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl2 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 1000 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | adantr 276 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: simpll2 1039 simprl2 1045 simp1l2 1093 simp2l2 1099 simp3l2 1105 3anandirs 1359 rspc3ev 2873 tfisi 4604 brcogw 4814 oawordi 6495 nnmord 6543 nnmword 6544 ac6sfi 6927 unsnfi 6948 unsnfidcel 6950 ordiso2 7065 prarloclemarch2 7449 enq0tr 7464 distrlem4prl 7614 distrlem4pru 7615 ltaprg 7649 aptiprlemu 7670 lelttr 8077 ltletr 8078 readdcan 8128 addcan 8168 addcan2 8169 ltadd2 8407 ltmul1a 8579 ltmul1 8580 divmulassap 8683 divmulasscomap 8684 lemul1a 8846 xrlelttr 9838 xrltletr 9839 xaddass 9901 xleadd1a 9905 xltadd1 9908 xlesubadd 9915 ixxdisj 9935 icoshftf1o 10023 icodisj 10024 lincmb01cmp 10035 iccf1o 10036 fztri3or 10071 ioom 10293 modqmuladdim 10400 modqmuladdnn0 10401 q2submod 10418 modqaddmulmod 10424 exp3val 10556 ltexp2a 10606 exple1 10610 expnbnd 10678 expnlbnd2 10680 nn0ltexp2 10724 nn0leexp2 10725 mulsubdivbinom2ap 10726 expcan 10731 fiprsshashgt1 10832 maxleastb 11258 maxltsup 11262 xrltmaxsup 11300 xrmaxltsup 11301 xrmaxaddlem 11303 xrmaxadd 11304 addcn2 11353 mulcn2 11355 geoisum1c 11563 dvdsval2 11832 dvdsmodexp 11837 dvdsadd2b 11882 dvdsaddre2b 11883 dvdsmod 11903 oexpneg 11917 divalglemex 11962 divalg 11964 gcdass 12051 rplpwr 12063 rppwr 12064 nnminle 12071 lcmass 12120 coprmdvds2 12128 rpmulgcd2 12130 rpdvds 12134 cncongr2 12139 rpexp 12188 znege1 12213 prmdiveq 12271 hashgcdlem 12273 odzdvds 12280 coprimeprodsq2 12293 pythagtriplem3 12302 pythagtriplem4 12303 pcdvdsb 12355 pcbc 12386 ctinf 12484 nninfdc 12507 isnsgrp 12884 issubmnd 12918 nmzsubg 13166 ghmnsgima 13224 srg1zr 13358 ring1eq0 13417 mulgass2 13427 rhmdvdsr 13542 rmodislmod 13684 topssnei 14139 cnptopco 14199 cnconst2 14210 cnptoprest 14216 cnpdis 14219 upxp 14249 bldisj 14378 blgt0 14379 bl2in 14380 blss2ps 14383 blss2 14384 xblm 14394 blssps 14404 blss 14405 xmetresbl 14417 bdbl 14480 bdmopn 14481 metcnp3 14488 metcnp 14489 metcnp2 14490 dvfvalap 14627 dvcnp2cntop 14640 dvcn 14641 logdivlti 14779 ltexp2 14837 lgsfvalg 14884 lgsneg 14903 lgsdilem 14906 lgsdirprm 14913 lgsdir 14914 lgsdi 14916 lgsne0 14917 1dom1el 15221 |
Copyright terms: Public domain | W3C validator |