Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp-4r | GIF version |
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
simp-4r | ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpllr 529 | . 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 274 | 1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 is referenced by: simp-5r 539 fimax2gtri 6875 finexdc 6876 dcfi 6954 difinfsn 7073 nnnninfeq2 7101 nninfisol 7105 exmidfodomrlemr 7166 exmidfodomrlemrALT 7167 suplocexprlemru 7668 suplocsrlemb 7755 suplocsrlem 7757 supinfneg 9541 infsupneg 9542 xaddf 9788 xaddval 9789 nn0ltexp2 10631 hashunlem 10726 xrmaxiflemcl 11195 xrmaxiflemlub 11198 xrmaxltsup 11208 sumeq2 11309 fsumconst 11404 prodeq2 11507 fprodconst 11570 sgrpidmndm 12643 cncnp 12983 neitx 13021 dedekindeulemlu 13352 suplociccreex 13355 dedekindicclemlu 13361 cnplimclemr 13391 limccnp2cntop 13399 logbgcd1irrap 13641 lgsval 13658 |
Copyright terms: Public domain | W3C validator |