![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp3l | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3l | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 109 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒) | |
2 | 1 | 3ad2ant3 1020 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
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 980 |
This theorem is referenced by: simpl3l 1052 simpr3l 1058 simp13l 1112 simp23l 1118 simp33l 1124 issod 4319 tfisi 4586 tfrlem5 6314 tfrlemibxssdm 6327 tfr1onlembxssdm 6343 tfrcllembxssdm 6356 ecopovtrn 6631 ecopovtrng 6634 dftap2 7249 addassnqg 7380 ltsonq 7396 ltanqg 7398 ltmnqg 7399 addassnq0 7460 mulasssrg 7756 distrsrg 7757 lttrsr 7760 ltsosr 7762 ltasrg 7768 mulextsr1lem 7778 mulextsr1 7779 axmulass 7871 axdistr 7872 lemul1 8548 reapmul1lem 8549 reapmul1 8550 mulcanap 8620 mulcanap2 8621 divassap 8645 divdirap 8652 div11ap 8655 muldivdirap 8662 divcanap5 8669 apmul1 8743 apmul2 8744 ltdiv1 8823 ltmuldiv 8829 ledivmul 8832 lemuldiv 8836 ltdiv2 8842 lediv2 8846 ltdiv23 8847 lediv23 8848 xaddass2 9868 xlt2add 9878 modqdi 10389 expaddzap 10561 expmulzap 10563 leisorel 10812 resqrtcl 11033 xrbdtri 11279 dvdscmulr 11822 dvdsmulcr 11823 dvdsadd2b 11842 dvdsgcd 12007 rpexp12i 12149 pythagtriplem3 12261 pcpremul 12287 pceu 12289 pcqmul 12297 pcqdiv 12301 f1ocpbllem 12713 cmn4 13061 ablsub4 13069 abladdsub4 13070 psmetlecl 13727 xmetlecl 13760 |
Copyright terms: Public domain | W3C validator |