![]() |
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 983 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 943 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 945 |
This theorem is referenced by: simpl1r 1014 simpr1r 1020 simp11r 1074 simp21r 1080 simp31r 1086 vtoclgft 2705 en2lp 4427 funprg 5129 nnsucsssuc 6340 ecopovtrn 6478 ecopovtrng 6481 addassnqg 7132 distrnqg 7137 ltsonq 7148 ltanqg 7150 ltmnqg 7151 distrnq0 7209 addassnq0 7212 prarloclem5 7250 recexprlem1ssl 7383 recexprlem1ssu 7384 mulasssrg 7495 distrsrg 7496 lttrsr 7499 ltsosr 7501 ltasrg 7507 mulextsr1lem 7516 mulextsr1 7517 axmulass 7602 axdistr 7603 dmdcanap 8389 lt2msq1 8547 lediv2 8553 xaddass2 9540 xlt2add 9550 modqdi 10052 expaddzaplem 10223 expaddzap 10224 expmulzap 10226 bdtrilem 10896 xrbdtri 10931 prmexpb 11669 cnptoprest 12244 ssblps 12408 ssbl 12409 |
Copyright terms: Public domain | W3C validator |