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 983 | . 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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: simpll3 1022 simprl3 1028 simp1l3 1076 simp2l3 1082 simp3l3 1088 3anandirs 1326 frirrg 4267 fcofo 5678 acexmid 5766 rdgon 6276 oawordi 6358 nnmord 6406 nnmword 6407 fidifsnen 6757 dif1en 6766 ac6sfi 6785 difinfsn 6978 enq0tr 7235 distrlem4prl 7385 distrlem4pru 7386 ltaprg 7420 lelttr 7845 ltletr 7846 readdcan 7895 addcan 7935 addcan2 7936 ltadd2 8174 divmulassap 8448 xrlelttr 9582 xrltletr 9583 xaddass 9645 xleadd1a 9649 xlesubadd 9659 icoshftf1o 9767 difelfzle 9904 fzo1fzo0n0 9953 modqmuladdim 10133 modqmuladdnn0 10134 modqm1p1mod0 10141 q2submod 10151 modifeq2int 10152 modqaddmulmod 10157 ltexp2a 10338 exple1 10342 expnlbnd2 10410 expcan 10456 fiprsshashgt1 10556 maxleastb 10979 maxltsup 10983 xrltmaxsup 11019 xrmaxltsup 11020 xrmaxaddlem 11022 xrmaxadd 11023 addcn2 11072 mulcn2 11074 isumz 11151 modmulconst 11514 dvdsmod 11549 divalglemex 11608 divalg 11610 gcdass 11692 rplpwr 11704 rppwr 11705 rpmulgcd2 11765 rpdvds 11769 rpexp 11820 znege1 11845 hashgcdlem 11892 ctinf 11932 neiint 12303 topssnei 12320 cnptopco 12380 cnrest2 12394 cnptoprest 12397 upxp 12430 bldisj 12559 blgt0 12560 bl2in 12561 blss2ps 12564 blss2 12565 xblm 12575 blssps 12585 blss 12586 bdmopn 12662 metcnp2 12671 txmetcnp 12676 cncfmptc 12740 dvcnp2cntop 12821 dvcn 12822 |
Copyright terms: Public domain | W3C validator |