Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpr3 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 988 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
2 | 1 | adantl 275 | 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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: simplr3 1030 simprr3 1036 simp1r3 1084 simp2r3 1090 simp3r3 1096 3anandis 1336 isopolem 5784 tfrlemibacc 6285 tfrlemibxssdm 6286 tfrlemibfn 6287 tfr1onlembacc 6301 tfr1onlembxssdm 6302 tfr1onlembfn 6303 tfrcllembacc 6314 tfrcllembxssdm 6315 tfrcllembfn 6316 elfir 6929 prloc 7423 prmuloc2 7499 ltntri 8017 eluzuzle 9465 xlesubadd 9810 elioc2 9863 elico2 9864 elicc2 9865 fseq1p1m1 10019 seq3f1olemp 10427 seq3f1oleml 10428 bcval5 10665 hashdifpr 10722 isumss2 11320 tanaddap 11666 dvds2ln 11750 divalglemeunn 11843 divalglemex 11844 divalglemeuneg 11845 restopnb 12728 icnpimaex 12758 cnptopresti 12785 psmettri 12877 isxmet2d 12895 xmettri 12919 metrtri 12924 xmetres2 12926 bldisj 12948 blss2ps 12953 blss2 12954 xmstri2 13017 mstri2 13018 xmstri 13019 mstri 13020 xmstri3 13021 mstri3 13022 msrtri 13023 comet 13046 bdbl 13050 xmetxp 13054 dvconst 13208 |
Copyright terms: Public domain | W3C validator |