![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simprll | GIF version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprll | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antrl 475 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 is referenced by: imain 5130 fcof1 5600 mpt20 5756 eroveu 6423 sbthlemi6 6751 sbthlemi8 6753 addcmpblnq 7023 mulcmpblnq 7024 ordpipqqs 7030 addcmpblnq0 7099 mulcmpblnq0 7100 nnnq0lem1 7102 prarloclemcalc 7158 addlocpr 7192 distrlem4prl 7240 distrlem4pru 7241 ltpopr 7251 addcmpblnr 7382 mulcmpblnrlemg 7383 mulcmpblnr 7384 prsrlem1 7385 ltsrprg 7390 apreap 8161 apreim 8177 divdivdivap 8277 divmuleqap 8281 divadddivap 8291 divsubdivap 8292 ledivdiv 8448 lediv12a 8452 exbtwnz 9811 seq3caopr 10033 leexp2r 10124 zfz1iso 10361 recvguniq 10543 rsqrmo 10575 summodclem2 10925 qredeu 11506 pw2dvdseu 11573 epttop 11942 metequiv2 12282 mulc1cncf 12344 cncfmptc 12348 cncfmptid 12349 addccncf 12351 negcncf 12353 |
Copyright terms: Public domain | W3C validator |