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 481 | 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 5200 fcof1 5677 fliftfun 5690 sbthlemi6 6843 sbthlemi8 6845 addcmpblnq 7168 mulcmpblnq 7169 ordpipqqs 7175 enq0tr 7235 addcmpblnq0 7244 mulcmpblnq0 7245 nnnq0lem1 7247 addnq0mo 7248 mulnq0mo 7249 prarloclemcalc 7303 addlocpr 7337 distrlem4prl 7385 distrlem4pru 7386 addcmpblnr 7540 mulcmpblnrlemg 7541 mulcmpblnr 7542 prsrlem1 7543 addsrmo 7544 mulsrmo 7545 ltsrprg 7548 apreap 8342 apreim 8358 divdivdivap 8466 divsubdivap 8481 ledivdiv 8641 lediv12a 8645 exbtwnz 10021 seq3caopr 10249 leexp2r 10340 zfz1iso 10577 recvguniq 10760 rsqrmo 10792 summodclem2 11144 qredeu 11767 pw2dvdseu 11835 epttop 12248 txdis1cn 12436 metequiv2 12654 cncfmptc 12740 cncfmptid 12741 addccncf 12744 negcncf 12746 dedekindicclemicc 12768 |
Copyright terms: Public domain | W3C validator |