Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simprll | Unicode 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 482 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 5264 fcof1 5745 mpo0 5903 eroveu 6583 sbthlemi6 6918 sbthlemi8 6920 addcmpblnq 7299 mulcmpblnq 7300 ordpipqqs 7306 addcmpblnq0 7375 mulcmpblnq0 7376 nnnq0lem1 7378 prarloclemcalc 7434 addlocpr 7468 distrlem4prl 7516 distrlem4pru 7517 ltpopr 7527 addcmpblnr 7671 mulcmpblnrlemg 7672 mulcmpblnr 7673 prsrlem1 7674 ltsrprg 7679 apreap 8476 apreim 8492 divdivdivap 8600 divmuleqap 8604 divadddivap 8614 divsubdivap 8615 ledivdiv 8776 lediv12a 8780 exbtwnz 10176 seq3caopr 10408 leexp2r 10499 zfz1iso 10740 recvguniq 10923 rsqrmo 10955 summodclem2 11309 prodmodc 11505 qredeu 12008 pw2dvdseu 12079 pcadd 12250 epttop 12637 txdis1cn 12825 metequiv2 13043 mulc1cncf 13123 cncfmptc 13129 cncfmptid 13130 addccncf 13133 negcncf 13135 dedekindicclemicc 13157 |
Copyright terms: Public domain | W3C validator |