![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1l | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp1l | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 109 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | 3ad2ant1 1018 | 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: simpl1l 1048 simpr1l 1054 simp11l 1108 simp21l 1114 simp31l 1120 en2lp 4552 tfisi 4585 funprg 5265 nnsucsssuc 6490 ecopovtrn 6629 ecopovtrng 6632 addassnqg 7378 distrnqg 7383 ltsonq 7394 ltanqg 7396 ltmnqg 7397 distrnq0 7455 addassnq0 7458 mulasssrg 7754 distrsrg 7755 lttrsr 7758 ltsosr 7760 ltasrg 7766 mulextsr1lem 7776 mulextsr1 7777 axmulass 7869 axdistr 7870 dmdcanap 8675 lt2msq1 8838 ltdiv2 8840 lediv2 8844 xaddass 9865 xaddass2 9866 xlt2add 9876 modqdi 10387 expaddzaplem 10558 expaddzap 10559 expmulzap 10561 resqrtcl 11031 bdtrilem 11240 bdtri 11241 xrbdtri 11277 prmexpb 12143 opprringbg 13181 cnptoprest 13610 ssblps 13796 ssbl 13797 rplogbchbase 14239 rplogbreexp 14242 relogbcxpbap 14254 lgssq 14312 |
Copyright terms: Public domain | W3C validator |