Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl1 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl1 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 986 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | adantr 274 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: simpll1 1025 simprl1 1031 simp1l1 1079 simp2l1 1085 simp3l1 1091 3anandirs 1337 rspc3ev 2842 brcogw 4767 cocan1 5749 oawordi 6428 nnmord 6476 nnmword 6477 dif1en 6836 ac6sfi 6855 ordiso2 6991 difinfsn 7056 ctssdc 7069 enq0tr 7366 distrlem4prl 7516 distrlem4pru 7517 ltaprg 7551 aptiprlemu 7572 lelttr 7978 readdcan 8029 addcan 8069 addcan2 8070 ltadd2 8308 ltmul1a 8480 ltmul1 8481 divmulassap 8582 divmulasscomap 8583 lemul1a 8744 xrlelttr 9733 xleadd1a 9800 xlesubadd 9810 icoshftf1o 9918 lincmb01cmp 9930 iccf1o 9931 fztri3or 9964 fzofzim 10113 ioom 10186 modqmuladdim 10292 modqm1p1mod0 10300 q2submod 10310 modqaddmulmod 10316 ltexp2a 10497 exple1 10501 expnlbnd2 10569 nn0ltexp2 10612 nn0leexp2 10613 expcan 10618 fiprsshashgt1 10719 fimaxq 10729 maxleastb 11142 maxltsup 11146 xrltmaxsup 11184 xrmaxltsup 11185 xrmaxaddlem 11187 addcn2 11237 mulcn2 11239 dvdsmodexp 11721 dvdsadd2b 11765 dvdsmod 11785 oexpneg 11799 divalglemex 11844 divalg 11846 gcdass 11933 rplpwr 11945 rppwr 11946 coprmdvds2 12004 rpmulgcd2 12006 qredeq 12007 rpdvds 12010 cncongr2 12015 rpexp 12064 znege1 12089 prmdiveq 12147 hashgcdlem 12149 odzdvds 12156 modprmn0modprm0 12167 coprimeprodsq2 12169 pythagtriplem3 12178 pcdvdsb 12230 pcgcd1 12238 qexpz 12261 pockthg 12266 ctinf 12306 nninfdc 12331 unbendc 12332 neiint 12692 topssnei 12709 iscnp4 12765 cnptopco 12769 cnconst2 12780 cnrest2 12783 cnptoprest 12786 cnpdis 12789 bldisj 12948 blgt0 12949 bl2in 12950 blss2ps 12953 blss2 12954 xblm 12964 blssps 12974 blss 12975 xmetresbl 12987 bdbl 13050 metcnp3 13058 metcnp2 13060 cncfmptc 13129 dvcnp2cntop 13210 dvcn 13211 logdivlti 13349 ltexp2 13407 |
Copyright terms: Public domain | W3C validator |