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 994 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | adantr 274 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
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 975 |
This theorem is referenced by: simpll3 1033 simprl3 1039 simp1l3 1087 simp2l3 1093 simp3l3 1099 3anandirs 1343 frirrg 4335 fcofo 5763 acexmid 5852 rdgon 6365 oawordi 6448 nnmord 6496 nnmword 6497 fidifsnen 6848 dif1en 6857 ac6sfi 6876 difinfsn 7077 enq0tr 7396 distrlem4prl 7546 distrlem4pru 7547 ltaprg 7581 lelttr 8008 ltletr 8009 readdcan 8059 addcan 8099 addcan2 8100 ltadd2 8338 divmulassap 8612 xrlelttr 9763 xrltletr 9764 xaddass 9826 xleadd1a 9830 xlesubadd 9840 icoshftf1o 9948 difelfzle 10090 fzo1fzo0n0 10139 modqmuladdim 10323 modqmuladdnn0 10324 modqm1p1mod0 10331 q2submod 10341 modifeq2int 10342 modqaddmulmod 10347 ltexp2a 10528 exple1 10532 expnlbnd2 10601 nn0ltexp2 10644 nn0leexp2 10645 expcan 10650 fiprsshashgt1 10752 maxleastb 11178 maxltsup 11182 xrltmaxsup 11220 xrmaxltsup 11221 xrmaxaddlem 11223 xrmaxadd 11224 addcn2 11273 mulcn2 11275 isumz 11352 dvdsmodexp 11757 modmulconst 11785 dvdsmod 11822 divalglemex 11881 divalg 11883 gcdass 11970 rplpwr 11982 rppwr 11983 nnwodc 11991 uzwodc 11992 rpmulgcd2 12049 rpdvds 12053 rpexp 12107 znege1 12132 prmdiveq 12190 hashgcdlem 12192 coprimeprodsq 12211 coprimeprodsq2 12212 pythagtriplem3 12221 pcdvdsb 12273 pcgcd1 12281 dvdsprmpweq 12288 pcbc 12303 ctinf 12385 nninfdc 12408 isnsgrp 12647 neiint 12939 topssnei 12956 cnptopco 13016 cnrest2 13030 cnptoprest 13033 upxp 13066 bldisj 13195 blgt0 13196 bl2in 13197 blss2ps 13200 blss2 13201 xblm 13211 blssps 13221 blss 13222 bdmopn 13298 metcnp2 13307 txmetcnp 13312 cncfmptc 13376 dvcnp2cntop 13457 dvcn 13458 logdivlti 13596 ltexp2 13654 lgsfvalg 13700 lgsneg 13719 lgsmod 13721 lgsdilem 13722 lgsdirprm 13729 lgsdir 13730 lgsdi 13732 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |