![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2l | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp2l | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 971 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: simpl2l 1002 simpr2l 1008 simp12l 1062 simp22l 1068 simp32l 1074 issod 4179 funprg 5109 fsnunf 5552 f1oiso2 5660 ecopovtrn 6456 ecopovtrng 6459 addassnqg 7091 ltsonq 7107 ltanqg 7109 ltmnqg 7110 addassnq0 7171 recexprlem1ssu 7343 mulasssrg 7454 distrsrg 7455 lttrsr 7458 ltsosr 7460 ltasrg 7466 mulextsr1lem 7475 mulextsr1 7476 axmulass 7558 axdistr 7559 dmdcanap 8343 ltdiv2 8503 lediv2 8507 ltdiv23 8508 lediv23 8509 xaddass 9493 xaddass2 9494 xlt2add 9504 expaddzaplem 10177 expaddzap 10178 expmulzap 10180 expdivap 10185 leisorel 10421 bdtrilem 10849 bdtri 10850 xrbdtri 10884 fsumsplitsnun 11027 prmexpb 11622 cnptoprest 12189 ssblps 12353 ssbl 12354 tgqioo 12466 |
Copyright terms: Public domain | W3C validator |