![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simprlr | Unicode version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprlr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad2antrl 482 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 is referenced by: imain 5213 fcof1 5692 fliftfun 5705 sbthlemi6 6858 sbthlemi8 6860 addcmpblnq 7199 mulcmpblnq 7200 ordpipqqs 7206 enq0tr 7266 addcmpblnq0 7275 mulcmpblnq0 7276 nnnq0lem1 7278 addnq0mo 7279 mulnq0mo 7280 prarloclemcalc 7334 addlocpr 7368 distrlem4prl 7416 distrlem4pru 7417 addcmpblnr 7571 mulcmpblnrlemg 7572 mulcmpblnr 7573 prsrlem1 7574 addsrmo 7575 mulsrmo 7576 ltsrprg 7579 apreap 8373 apreim 8389 divdivdivap 8497 divsubdivap 8512 ledivdiv 8672 lediv12a 8676 exbtwnz 10059 seq3caopr 10287 leexp2r 10378 zfz1iso 10616 recvguniq 10799 rsqrmo 10831 summodclem2 11183 prodmodclem2 11378 prodmodc 11379 qredeu 11814 pw2dvdseu 11882 epttop 12298 txdis1cn 12486 metequiv2 12704 cncfmptc 12790 cncfmptid 12791 addccncf 12794 negcncf 12796 dedekindicclemicc 12818 |
Copyright terms: Public domain | W3C validator |