![]() |
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 107 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | 3ad2ant1 960 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simpl1l 990 simpr1l 996 simp11l 1050 simp21l 1056 simp31l 1062 en2lp 4325 tfisi 4356 funprg 5000 nnsucsssuc 6156 ecopovtrn 6290 ecopovtrng 6293 addassnqg 6686 distrnqg 6691 ltsonq 6702 ltanqg 6704 ltmnqg 6705 distrnq0 6763 addassnq0 6766 mulasssrg 7049 distrsrg 7050 lttrsr 7053 ltsosr 7055 ltasrg 7061 mulextsr1lem 7070 mulextsr1 7071 axmulass 7153 axdistr 7154 dmdcanap 7929 lt2msq1 8082 ltdiv2 8084 lediv2 8088 modqdi 9526 expaddzaplem 9668 expaddzap 9669 expmulzap 9671 resqrtcl 10116 prmexpb 10737 |
Copyright terms: Public domain | W3C validator |