![]() |
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 534 | . 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 276 | 1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: simp-5r 544 fimax2gtri 6929 finexdc 6930 dcfi 7010 difinfsn 7129 nnnninfeq2 7157 nninfisol 7161 exmidfodomrlemr 7231 exmidfodomrlemrALT 7232 suplocexprlemru 7748 suplocsrlemb 7835 suplocsrlem 7837 aptap 8637 supinfneg 9625 infsupneg 9626 xaddf 9874 xaddval 9875 nn0ltexp2 10721 hashunlem 10816 xrmaxiflemcl 11285 xrmaxiflemlub 11288 xrmaxltsup 11298 sumeq2 11399 fsumconst 11494 prodeq2 11597 fprodconst 11660 sgrpidmndm 12881 mhmmnd 13058 ghmcmn 13265 issrg 13319 cncnp 14187 neitx 14225 dedekindeulemlu 14556 suplociccreex 14559 dedekindicclemlu 14565 cnplimclemr 14595 limccnp2cntop 14603 logbgcd1irrap 14845 lgsval 14863 |
Copyright terms: Public domain | W3C validator |