![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpl3 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl3 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 941 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | adantr 270 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simpll3 980 simprl3 986 simp1l3 1034 simp2l3 1040 simp3l3 1046 3anandirs 1280 frirrg 4107 fcofo 5449 acexmid 5536 rdgon 6029 oawordi 6107 nnmord 6149 nnmword 6150 fidifsnen 6395 dif1en 6404 ac6sfi 6421 enq0tr 6675 distrlem4prl 6825 distrlem4pru 6826 ltaprg 6860 lelttr 7255 ltletr 7256 readdcan 7304 addcan 7344 addcan2 7345 ltadd2 7579 divmulassap 7839 xrlelttr 8941 xrltletr 8942 icoshftf1o 9078 difelfzle 9211 fzo1fzo0n0 9258 modqmuladdim 9438 modqmuladdnn0 9439 modqm1p1mod0 9446 q2submod 9456 modifeq2int 9457 modqaddmulmod 9462 ltexp2a 9614 exple1 9618 expnlbnd2 9684 expcan 9730 maxleastb 10227 maxltsup 10231 addcn2 10276 mulcn2 10278 modmulconst 10361 dvdsmod 10396 divalglemex 10455 divalg 10457 gcdass 10537 rplpwr 10549 rppwr 10550 rpmulgcd2 10610 rpdvds 10614 rpexp 10665 znege1 10689 |
Copyright terms: Public domain | W3C validator |