Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an4s | Unicode version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an4s.1 |
Ref | Expression |
---|---|
an4s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an4 520 | . 2 | |
2 | an4s.1 | . 2 | |
3 | 1, 2 | sylbi 114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: an42s 523 anandis 526 anandirs 527 trin2 4716 fnun 5005 2elresin 5010 f1co 5101 f1oun 5146 f1oco 5149 f1mpt 5410 poxp 5853 tfrlem7 5933 brecop 6196 th3qlem1 6208 oviec 6212 addcmpblnq 6465 mulcmpblnq 6466 mulpipqqs 6471 mulclnq 6474 mulcanenq 6483 distrnqg 6485 mulcmpblnq0 6542 mulcanenq0ec 6543 mulclnq0 6550 nqnq0a 6552 nqnq0m 6553 distrnq0 6557 genipv 6607 genpelvl 6610 genpelvu 6611 genpml 6615 genpmu 6616 genpcdl 6617 genpcuu 6618 genprndl 6619 genprndu 6620 distrlem1prl 6680 distrlem1pru 6681 ltsopr 6694 addcmpblnr 6824 ltsrprg 6832 addclsr 6838 mulclsr 6839 addasssrg 6841 addresr 6913 mulresr 6914 axaddass 6946 axmulass 6947 axdistr 6948 mulgt0 7093 mul4 7145 add4 7172 2addsub 7225 addsubeq4 7226 sub4 7256 muladd 7381 mulsub 7398 add20i 7484 mulge0i 7611 mulap0b 7636 divmuldivap 7688 ltmul12a 7826 zmulcl 8297 uz2mulcl 8545 qaddcl 8570 qmulcl 8572 qreccl 8576 rpaddcl 8606 ge0addcl 8850 serige0 9252 expge1 9292 rexanuz 9587 amgm2 9714 mulcn2 9833 bj-indind 10056 |
Copyright terms: Public domain | W3C validator |