![]() |
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 107 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 961 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simpl2l 992 simpr2l 998 simp12l 1052 simp22l 1058 simp32l 1064 issod 4082 funprg 4980 fsnunf 5394 f1oiso2 5497 ecopovtrn 6269 ecopovtrng 6272 addassnqg 6634 ltsonq 6650 ltanqg 6652 ltmnqg 6653 addassnq0 6714 recexprlem1ssu 6886 mulasssrg 6997 distrsrg 6998 lttrsr 7001 ltsosr 7003 ltasrg 7009 mulextsr1lem 7018 mulextsr1 7019 axmulass 7101 axdistr 7102 dmdcanap 7877 ltdiv2 8032 lediv2 8036 ltdiv23 8037 lediv23 8038 expaddzaplem 9616 expaddzap 9617 expmulzap 9619 expdivap 9624 prmexpb 10674 |
Copyright terms: Public domain | W3C validator |