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 108 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | 3ad2ant1 987 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: simpl1l 1017 simpr1l 1023 simp11l 1077 simp21l 1083 simp31l 1089 en2lp 4439 tfisi 4471 funprg 5143 nnsucsssuc 6356 ecopovtrn 6494 ecopovtrng 6497 addassnqg 7158 distrnqg 7163 ltsonq 7174 ltanqg 7176 ltmnqg 7177 distrnq0 7235 addassnq0 7238 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltsosr 7540 ltasrg 7546 mulextsr1lem 7556 mulextsr1 7557 axmulass 7649 axdistr 7650 dmdcanap 8450 lt2msq1 8611 ltdiv2 8613 lediv2 8617 xaddass 9620 xaddass2 9621 xlt2add 9631 modqdi 10133 expaddzaplem 10304 expaddzap 10305 expmulzap 10307 resqrtcl 10769 bdtrilem 10978 bdtri 10979 xrbdtri 11013 prmexpb 11756 cnptoprest 12335 ssblps 12521 ssbl 12522 |
Copyright terms: Public domain | W3C validator |