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 576 | . 2 | |
2 | an4s.1 | . 2 | |
3 | 1, 2 | sylbi 120 | 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 depends on definitions: df-bi 116 |
This theorem is referenced by: an42s 579 anandis 582 anandirs 583 trin2 4989 fnun 5288 2elresin 5293 f1co 5399 f1oun 5446 f1oco 5449 f1mpt 5733 poxp 6191 tfrlem7 6276 brecop 6582 th3qlem1 6594 oviec 6598 pmss12g 6632 addcmpblnq 7299 mulcmpblnq 7300 mulpipqqs 7305 mulclnq 7308 mulcanenq 7317 distrnqg 7319 mulcmpblnq0 7376 mulcanenq0ec 7377 mulclnq0 7384 nqnq0a 7386 nqnq0m 7387 distrnq0 7391 genipv 7441 genpelvl 7444 genpelvu 7445 genpml 7449 genpmu 7450 genpcdl 7451 genpcuu 7452 genprndl 7453 genprndu 7454 distrlem1prl 7514 distrlem1pru 7515 ltsopr 7528 addcmpblnr 7671 ltsrprg 7679 addclsr 7685 mulclsr 7686 addasssrg 7688 addresr 7769 mulresr 7770 axaddass 7804 axmulass 7805 axdistr 7806 mulgt0 7964 mul4 8021 add4 8050 2addsub 8103 addsubeq4 8104 sub4 8134 muladd 8273 mulsub 8290 add20i 8381 mulge0i 8509 mulap0b 8543 divmuldivap 8599 ltmul12a 8746 zmulcl 9235 uz2mulcl 9537 qaddcl 9564 qmulcl 9566 qreccl 9571 rpaddcl 9604 ge0addcl 9908 ge0xaddcl 9910 expge1 10482 rexanuz 10916 amgm2 11046 iooinsup 11204 mulcn2 11239 dvds2ln 11750 opoe 11817 omoe 11818 opeo 11819 omeo 11820 lcmgcd 11989 lcmdvds 11990 pc2dvds 12240 tgcl 12611 innei 12710 txbas 12805 txss12 12813 txbasval 12814 blsscls2 13040 qtopbasss 13068 bj-indind 13655 |
Copyright terms: Public domain | W3C validator |