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 108 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 988 | 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: simpl2l 1019 simpr2l 1025 simp12l 1079 simp22l 1085 simp32l 1091 issod 4211 funprg 5143 fsnunf 5588 f1oiso2 5696 ecopovtrn 6494 ecopovtrng 6497 addassnqg 7158 ltsonq 7174 ltanqg 7176 ltmnqg 7177 addassnq0 7238 recexprlem1ssu 7410 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltsosr 7540 ltasrg 7546 mulextsr1lem 7556 mulextsr1 7557 axmulass 7649 axdistr 7650 dmdcanap 8450 ltdiv2 8613 lediv2 8617 ltdiv23 8618 lediv23 8619 xaddass 9620 xaddass2 9621 xlt2add 9631 expaddzaplem 10304 expaddzap 10305 expmulzap 10307 expdivap 10312 leisorel 10548 bdtrilem 10978 bdtri 10979 xrbdtri 11013 fsumsplitsnun 11156 prmexpb 11756 cnptoprest 12335 ssblps 12521 ssbl 12522 tgqioo 12643 |
Copyright terms: Public domain | W3C validator |