Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp2r | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp2r | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 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: simpl2r 1020 simpr2r 1026 simp12r 1080 simp22r 1086 simp32r 1092 issod 4211 funprg 5143 fsnunf 5588 f1oiso2 5696 tfrlemibxssdm 6192 ecopovtrn 6494 ecopovtrng 6497 addassnqg 7158 ltsonq 7174 ltanqg 7176 ltmnqg 7177 addassnq0 7238 recexprlem1ssl 7409 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltsosr 7540 ltasrg 7546 mulextsr1lem 7556 mulextsr1 7557 axmulass 7649 axdistr 7650 dmdcanap 8450 lediv2 8617 ltdiv23 8618 lediv23 8619 xaddass2 9621 xlt2add 9631 expaddzaplem 10304 expaddzap 10305 expmulzap 10307 expdivap 10312 leisorel 10548 bdtrilem 10978 xrbdtri 11013 fldivndvdslt 11559 prmexpb 11756 cnptoprest 12335 ssblps 12521 ssbl 12522 tgqioo 12643 |
Copyright terms: Public domain | W3C validator |