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 560 | . 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 563 anandis 566 anandirs 567 trin2 4900 fnun 5199 2elresin 5204 f1co 5310 f1oun 5355 f1oco 5358 f1mpt 5640 poxp 6097 tfrlem7 6182 brecop 6487 th3qlem1 6499 oviec 6503 pmss12g 6537 addcmpblnq 7143 mulcmpblnq 7144 mulpipqqs 7149 mulclnq 7152 mulcanenq 7161 distrnqg 7163 mulcmpblnq0 7220 mulcanenq0ec 7221 mulclnq0 7228 nqnq0a 7230 nqnq0m 7231 distrnq0 7235 genipv 7285 genpelvl 7288 genpelvu 7289 genpml 7293 genpmu 7294 genpcdl 7295 genpcuu 7296 genprndl 7297 genprndu 7298 distrlem1prl 7358 distrlem1pru 7359 ltsopr 7372 addcmpblnr 7515 ltsrprg 7523 addclsr 7529 mulclsr 7530 addasssrg 7532 addresr 7613 mulresr 7614 axaddass 7648 axmulass 7649 axdistr 7650 mulgt0 7807 mul4 7862 add4 7891 2addsub 7944 addsubeq4 7945 sub4 7975 muladd 8114 mulsub 8131 add20i 8222 mulge0i 8350 mulap0b 8384 divmuldivap 8440 ltmul12a 8586 zmulcl 9075 uz2mulcl 9370 qaddcl 9395 qmulcl 9397 qreccl 9402 rpaddcl 9433 ge0addcl 9732 ge0xaddcl 9734 expge1 10298 rexanuz 10728 amgm2 10858 iooinsup 11014 mulcn2 11049 dvds2ln 11453 opoe 11519 omoe 11520 opeo 11521 omeo 11522 lcmgcd 11686 lcmdvds 11687 tgcl 12160 innei 12259 txbas 12354 txss12 12362 txbasval 12363 blsscls2 12589 qtopbasss 12617 bj-indind 13057 |
Copyright terms: Public domain | W3C validator |