Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpr2 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 967 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒) | |
2 | 1 | adantl 275 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
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 949 |
This theorem is referenced by: simplr2 1009 simprr2 1015 simp1r2 1063 simp2r2 1069 simp3r2 1075 3anandis 1310 isopolem 5691 tfrlemibacc 6191 tfrlemibfn 6193 tfr1onlembacc 6207 tfr1onlembfn 6209 tfrcllembacc 6220 tfrcllembfn 6222 prltlu 7263 prdisj 7268 prmuloc2 7343 ltntri 7858 eluzuzle 9302 xlesubadd 9634 elioc2 9687 elico2 9688 elicc2 9689 fseq1p1m1 9842 fz0fzelfz0 9872 seq3f1olemp 10243 bcval5 10477 hashdifpr 10534 summodclem2 11119 isumss2 11130 tanaddap 11373 dvds2ln 11453 divalglemeunn 11545 divalglemex 11546 divalglemeuneg 11547 isstructr 11901 restopnb 12277 icnpimaex 12307 cnptopresti 12334 psmettri 12426 isxmet2d 12444 xmettri 12468 metrtri 12473 xmetres2 12475 bldisj 12497 blss2ps 12502 blss2 12503 xmstri2 12566 mstri2 12567 xmstri 12568 mstri 12569 xmstri3 12570 mstri3 12571 msrtri 12572 comet 12595 bdbl 12599 xmetxp 12603 dvconst 12757 |
Copyright terms: Public domain | W3C validator |