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 981 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | adantr 274 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
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 964 |
This theorem is referenced by: simpll1 1020 simprl1 1026 simp1l1 1074 simp2l1 1080 simp3l1 1086 3anandirs 1326 rspc3ev 2801 brcogw 4703 cocan1 5681 oawordi 6358 nnmord 6406 nnmword 6407 dif1en 6766 ac6sfi 6785 ordiso2 6913 difinfsn 6978 ctssdc 6991 enq0tr 7235 distrlem4prl 7385 distrlem4pru 7386 ltaprg 7420 aptiprlemu 7441 lelttr 7845 readdcan 7895 addcan 7935 addcan2 7936 ltadd2 8174 ltmul1a 8346 ltmul1 8347 divmulassap 8448 divmulasscomap 8449 lemul1a 8609 xrlelttr 9582 xleadd1a 9649 xlesubadd 9659 icoshftf1o 9767 lincmb01cmp 9779 iccf1o 9780 fztri3or 9812 fzofzim 9958 ioom 10031 modqmuladdim 10133 modqm1p1mod0 10141 q2submod 10151 modqaddmulmod 10157 ltexp2a 10338 exple1 10342 expnlbnd2 10410 expcan 10456 fiprsshashgt1 10556 fimaxq 10566 maxleastb 10979 maxltsup 10983 xrltmaxsup 11019 xrmaxltsup 11020 xrmaxaddlem 11022 addcn2 11072 mulcn2 11074 dvdsadd2b 11529 dvdsmod 11549 oexpneg 11563 divalglemex 11608 divalg 11610 gcdass 11692 rplpwr 11704 rppwr 11705 coprmdvds2 11763 rpmulgcd2 11765 qredeq 11766 rpdvds 11769 cncongr2 11774 rpexp 11820 znege1 11845 hashgcdlem 11892 ctinf 11932 neiint 12303 topssnei 12320 iscnp4 12376 cnptopco 12380 cnconst2 12391 cnrest2 12394 cnptoprest 12397 cnpdis 12400 bldisj 12559 blgt0 12560 bl2in 12561 blss2ps 12564 blss2 12565 xblm 12575 blssps 12585 blss 12586 xmetresbl 12598 bdbl 12661 metcnp3 12669 metcnp2 12671 cncfmptc 12740 dvcnp2cntop 12821 dvcn 12822 |
Copyright terms: Public domain | W3C validator |