Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp1r | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp1r | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 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: simpl1r 1018 simpr1r 1024 simp11r 1078 simp21r 1084 simp31r 1090 vtoclgft 2710 en2lp 4439 funprg 5143 nnsucsssuc 6356 ecopovtrn 6494 ecopovtrng 6497 addassnqg 7158 distrnqg 7163 ltsonq 7174 ltanqg 7176 ltmnqg 7177 distrnq0 7235 addassnq0 7238 prarloclem5 7276 recexprlem1ssl 7409 recexprlem1ssu 7410 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltsosr 7540 ltasrg 7546 mulextsr1lem 7556 mulextsr1 7557 axmulass 7649 axdistr 7650 dmdcanap 8450 lt2msq1 8611 lediv2 8617 xaddass2 9621 xlt2add 9631 modqdi 10133 expaddzaplem 10304 expaddzap 10305 expmulzap 10307 bdtrilem 10978 xrbdtri 11013 prmexpb 11756 cnptoprest 12335 ssblps 12521 ssbl 12522 |
Copyright terms: Public domain | W3C validator |