![]() |
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 940 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒) | |
2 | 1 | adantl 271 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simplr2 982 simprr2 988 simp1r2 1036 simp2r2 1042 simp3r2 1048 3anandis 1279 isopolem 5540 tfrlemibacc 6023 tfrlemibfn 6025 tfr1onlembacc 6039 tfr1onlembfn 6041 tfrcllembacc 6052 tfrcllembfn 6054 prltlu 6949 prdisj 6954 prmuloc2 7029 eluzuzle 8922 elioc2 9249 elico2 9250 elicc2 9251 fseq1p1m1 9401 fz0fzelfz0 9429 ibcval5 10006 hashdifpr 10063 dvds2ln 10609 divalglemeunn 10701 divalglemex 10702 divalglemeuneg 10703 |
Copyright terms: Public domain | W3C validator |