![]() |
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 108 | . 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: simpl2r 993 simpr2r 999 simp12r 1053 simp22r 1059 simp32r 1065 issod 4082 funprg 4980 fsnunf 5394 f1oiso2 5497 tfrlemibxssdm 5976 ecopovtrn 6269 ecopovtrng 6272 addassnqg 6634 ltsonq 6650 ltanqg 6652 ltmnqg 6653 addassnq0 6714 recexprlem1ssl 6885 mulasssrg 6997 distrsrg 6998 lttrsr 7001 ltsosr 7003 ltasrg 7009 mulextsr1lem 7018 mulextsr1 7019 axmulass 7101 axdistr 7102 dmdcanap 7877 lediv2 8036 ltdiv23 8037 lediv23 8038 expaddzaplem 9616 expaddzap 9617 expmulzap 9619 expdivap 9624 fldivndvdslt 10479 prmexpb 10674 |
Copyright terms: Public domain | W3C validator |