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 109 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | 3ad2ant2 1008 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
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 969 |
This theorem is referenced by: simpl2r 1040 simpr2r 1046 simp12r 1100 simp22r 1106 simp32r 1112 issod 4291 funprg 5232 fsnunf 5679 f1oiso2 5789 tfrlemibxssdm 6286 ecopovtrn 6589 ecopovtrng 6592 addassnqg 7314 ltsonq 7330 ltanqg 7332 ltmnqg 7333 addassnq0 7394 recexprlem1ssl 7565 mulasssrg 7690 distrsrg 7691 lttrsr 7694 ltsosr 7696 ltasrg 7702 mulextsr1lem 7712 mulextsr1 7713 axmulass 7805 axdistr 7806 dmdcanap 8609 lediv2 8777 ltdiv23 8778 lediv23 8779 xaddass2 9797 xlt2add 9807 expaddzaplem 10488 expaddzap 10489 expmulzap 10491 expdivap 10496 leisorel 10736 bdtrilem 11166 xrbdtri 11203 fldivndvdslt 11857 prmexpb 12062 pcpremul 12204 pcdiv 12213 pcqmul 12214 pcqdiv 12218 cnptoprest 12786 ssblps 12972 ssbl 12973 tgqioo 13094 rplogbchbase 13415 |
Copyright terms: Public domain | W3C validator |