Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an42s | Unicode version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an41r3s.1 |
Ref | Expression |
---|---|
an42s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an41r3s.1 | . . 3 | |
2 | 1 | an4s 583 | . 2 |
3 | 2 | ancom2s 561 | 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: nnmsucr 6464 ecopoveq 6604 enqdc 7310 addcmpblnq 7316 addpipqqslem 7318 addpipqqs 7319 addclnq 7324 addcomnqg 7330 distrnqg 7336 recexnq 7339 ltdcnq 7346 ltexnqq 7357 enq0enq 7380 enq0sym 7381 enq0breq 7385 addclnq0 7400 distrnq0 7408 mulclsr 7703 axmulass 7822 axdistr 7823 subadd4 8150 mulsub 8307 mgmidmo 12612 tgcl 12779 |
Copyright terms: Public domain | W3C validator |