![]() |
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 110 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
2 | 1 | 3ad2ant1 1019 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: simpl1r 1050 simpr1r 1056 simp11r 1110 simp21r 1116 simp31r 1122 vtoclgft 2799 en2lp 4565 funprg 5278 nnsucsssuc 6507 ecopovtrn 6646 ecopovtrng 6649 addassnqg 7395 distrnqg 7400 ltsonq 7411 ltanqg 7413 ltmnqg 7414 distrnq0 7472 addassnq0 7475 prarloclem5 7513 recexprlem1ssl 7646 recexprlem1ssu 7647 mulasssrg 7771 distrsrg 7772 lttrsr 7775 ltsosr 7777 ltasrg 7783 mulextsr1lem 7793 mulextsr1 7794 axmulass 7886 axdistr 7887 dmdcanap 8693 lt2msq1 8856 lediv2 8862 xaddass2 9884 xlt2add 9894 modqdi 10406 expaddzaplem 10577 expaddzap 10578 expmulzap 10580 bdtrilem 11261 xrbdtri 11298 prmexpb 12165 mgmsscl 12799 subgabl 13167 cnptoprest 14035 ssblps 14221 ssbl 14222 rplogbchbase 14664 rplogbreexp 14667 relogbcxpbap 14679 lgssq 14737 |
Copyright terms: Public domain | W3C validator |