![]() |
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 947 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | adantr 271 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: simpll2 986 simprl2 992 simp1l2 1040 simp2l2 1046 simp3l2 1052 3anandirs 1291 rspc3ev 2752 tfisi 4430 brcogw 4636 oawordi 6270 nnmord 6316 nnmword 6317 ac6sfi 6694 unsnfi 6709 unsnfidcel 6711 ordiso2 6808 prarloclemarch2 7075 enq0tr 7090 distrlem4prl 7240 distrlem4pru 7241 ltaprg 7275 aptiprlemu 7296 lelttr 7670 ltletr 7671 readdcan 7719 addcan 7759 addcan2 7760 ltadd2 7994 ltmul1a 8165 ltmul1 8166 divmulassap 8259 divmulasscomap 8260 lemul1a 8416 xrlelttr 9372 xrltletr 9373 xaddass 9435 xleadd1a 9439 xltadd1 9442 xlesubadd 9449 ixxdisj 9469 icoshftf1o 9557 icodisj 9558 lincmb01cmp 9569 iccf1o 9570 fztri3or 9602 ioom 9821 modqmuladdim 9923 modqmuladdnn0 9924 q2submod 9941 modqaddmulmod 9947 exp3val 10088 ltexp2a 10138 exple1 10142 expnbnd 10208 expnlbnd2 10210 expcan 10256 fiprsshashgt1 10356 maxleastb 10778 maxltsup 10782 xrltmaxsup 10816 xrmaxltsup 10817 xrmaxaddlem 10819 xrmaxadd 10820 addcn2 10869 mulcn2 10871 geoisum1c 11078 dvdsval2 11241 dvdsadd2b 11285 dvdsmod 11305 oexpneg 11319 divalglemex 11364 divalg 11366 gcdass 11446 rplpwr 11458 rppwr 11459 lcmass 11509 coprmdvds2 11517 rpmulgcd2 11519 rpdvds 11523 cncongr2 11528 rpexp 11574 znege1 11598 hashgcdlem 11645 topssnei 12029 cnptopco 12088 cnconst2 12099 cnptoprest 12105 cnpdis 12108 bldisj 12202 blgt0 12203 bl2in 12204 blss2ps 12207 blss2 12208 xblm 12218 blssps 12228 blss 12229 xmetresbl 12241 bdbl 12304 bdmopn 12305 metcnp3 12308 metcnp 12309 metcnp2 12310 |
Copyright terms: Public domain | W3C validator |