![]() |
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 109 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 1021 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
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 depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: simpl2l 1052 simpr2l 1058 simp12l 1112 simp22l 1118 simp32l 1124 issod 4337 funprg 5285 fsnunf 5736 f1oiso2 5848 ecopovtrn 6657 ecopovtrng 6660 dftap2 7279 addassnqg 7410 ltsonq 7426 ltanqg 7428 ltmnqg 7429 addassnq0 7490 recexprlem1ssu 7662 mulasssrg 7786 distrsrg 7787 lttrsr 7790 ltsosr 7792 ltasrg 7798 mulextsr1lem 7808 mulextsr1 7809 axmulass 7901 axdistr 7902 dmdcanap 8708 ltdiv2 8873 lediv2 8877 ltdiv23 8878 lediv23 8879 xaddass 9898 xaddass2 9899 xlt2add 9909 expaddzaplem 10593 expaddzap 10594 expmulzap 10596 expdivap 10601 leisorel 10848 bdtrilem 11278 bdtri 11279 xrbdtri 11315 fsumsplitsnun 11458 prmexpb 12182 pcpremul 12324 pcdiv 12333 pcqmul 12334 pcqdiv 12338 4sqlem12 12433 f1ocpbllem 12784 ercpbl 12804 erlecpbl 12805 cmn4 13241 ablsub4 13249 abladdsub4 13250 cnptoprest 14191 ssblps 14377 ssbl 14378 tgqioo 14499 rplogbchbase 14820 |
Copyright terms: Public domain | W3C validator |